FKS2.remark_after_corollary_11

@[blueprint  "fks2-remark-after-corollary-11"  (title := "FKS2 remark after Corollary 11")  (statement := /--  The Dawson function has a single maximum at $x \approx 0.942$, after which the function is  decreasing. -/)  (proof := /-- The Dawson function satisfies the differential equation $F'(x) + 2xF(x) = 1$ from which it follows that the second derivative satisfies $F''(x) = −2F(x) − 2x(−2xF(x) + 1)$, so that at every critical point (where we have $F(x) = \frac{1}{2x}$) we have $F''(x) = −\frac{1}{x}$.  It follows that every positive critical value gives a local maximum, hence there is a unique such critical value and the function decreases after it. Numerically one may verify this is near 0.9241 see https://oeis.org/ A133841. -/)  (latexEnv := "remark")  (discussion := 616)]theorem remark_after_corollary_11 :    ∃ x₀ : ℝ, x₀ ∈ Set.Icc 0.924 0.925 ∧ (∀ x, dawson x ≤ dawson x₀) ∧      StrictAntiOn dawson (Set.Ioi x₀) := by  obtain ⟨x₀, hx₀_pos, h_glob_max, h_crit⟩ := dawson_exists_critical_global_max  have h_crit_eq : 1 - 2 * x₀ * dawson x₀ = 0 := (deriv_dawson x₀).symm.trans h_crit  have h_deriv_pos_0924 : 1 - 2 * 0.924 * dawson 0.924 > 0 := by linarith [dawson_0924_bound]  have h_deriv_neg_0925 : 1 - 2 * 0.925 * dawson 0.925 < 0 := by linarith [dawson_0925_bound]  have h_ge_0924 : 0.924 ≤ x₀ :=    crit_ge_of_F_pos x₀ 0.924 hx₀_pos (by norm_num) h_crit_eq h_deriv_pos_0924  have h_le_0925 : x₀ ≤ 0.925 :=    crit_le_of_F_neg x₀ 0.925 hx₀_pos (by norm_num) h_crit_eq h_deriv_neg_0925  have h_deriv_neg : ∀ x ∈ Set.Ioi x₀, 1 - 2 * x * dawson x < 0 := by    intro x hx    have hF_lt := F_strictAnti hx₀_pos (lt_trans hx₀_pos hx) hx    dsimp at hF_lt    rw [h_crit_eq, mul_zero] at hF_lt    nlinarith [exp_pos (x ^ 2)]  refine ⟨x₀, ⟨h_ge_0924, h_le_0925⟩, h_glob_max,    strictAntiOn_of_deriv_neg (convex_Ioi x₀) continuous_dawson.continuousOn (fun x hx ↦ ?_)⟩  rw [interior_Ioi] at hx  rw [deriv_dawson]  exact h_deriv_neg x hx