Source indexedtheorem · leanprover/lean4:v4.32.0

FKS2.dawson_le_sharp

PrimeNumberTheoremAnd.IEANTN.FKS2 · PrimeNumberTheoremAnd/IEANTN/FKS2.lean:401 to 461

Source documentation

Sharp Dawson upper bound: for 0 ≤ w ≤ z, dawson z ≤ 1/(2z) + e^{w²}/(4z³) + (z−w)·e^{−w(2z−w)}.

Refines dawson x ≤ 1/x to the true leading term 1/(2z) with explicitly controlled corrections; a moderate w makes the last two terms negligible for large z. This is the estimate behind the numerical bound on μ_asymp in Corollary 22.

Exact Lean statement

theorem dawson_le_sharp {z w : ℝ} (hw0 : 0 ≤ w) (hwz : w ≤ z) (hz : 0 < z) :
    dawson z ≤ 1 / (2 * z) + exp (w ^ 2) / (4 * z ^ 3) +
      (z - w) * exp (-(w * (2 * z - w)))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem dawson_le_sharp {z w : ℝ} (hw0 : 0 ≤ w) (hwz : w ≤ z) (hz : 0 < z) :    dawson z ≤ 1 / (2 * z) + exp (w ^ 2) / (4 * z ^ 3) +      (z - w) * exp (-(w * (2 * z - w))) := by  rw [dawson_eq_integral]  have hint : ∀ a b : ℝ,      IntervalIntegrable (fun u => exp (u ^ 2 - 2 * z * u)) volume a b := by    intro a b    apply Continuous.intervalIntegrable    continuity  rw [← intervalIntegral.integral_add_adjacent_intervals (a := (0:ℝ)) (b := w) (c := z)    (hint 0 w) (hint w z)]  have head : (∫ u in (0:ℝ)..w, exp (u ^ 2 - 2 * z * u)) ≤      1 / (2 * z) + exp (w ^ 2) / (4 * z ^ 3) := by    have hptw : ∀ u ∈ Set.Icc (0:ℝ) w,        exp (u ^ 2 - 2 * z * u) ≤          exp (-(2 * z) * u) + exp (w ^ 2) * (u ^ 2 * exp (-(2 * z) * u)) := by      intro u hu      have hsplit : exp (u ^ 2 - 2 * z * u) = exp (u ^ 2) * exp (-(2 * z) * u) := by        rw [← Real.exp_add]        congr 1        ring      rw [hsplit]      have hb := exp_le_one_add_mul_exp (sq_nonneg u)        (by nlinarith [hu.1, hu.2] : u ^ 2 ≤ w ^ 2)      have hepos : (0:ℝ) ≤ exp (-(2 * z) * u) := exp_nonneg _      nlinarith [hb, hepos]    have hmono := intervalIntegral.integral_mono_on hw0 (hint 0 w)      (by apply Continuous.intervalIntegrable; continuity) hptw    have hlin : (∫ u in (0:ℝ)..w,          (exp (-(2 * z) * u) + exp (w ^ 2) * (u ^ 2 * exp (-(2 * z) * u)))) =        (∫ u in (0:ℝ)..w, exp (-(2 * z) * u)) +          exp (w ^ 2) * (∫ u in (0:ℝ)..w, u ^ 2 * exp (-(2 * z) * u)) := by      rw [intervalIntegral.integral_add        (by apply Continuous.intervalIntegrable; continuity)        (by apply Continuous.intervalIntegrable; continuity),        intervalIntegral.integral_const_mul]    have hgeom := integral_exp_neg_mul_le (w := w) hz    have hsq := integral_sq_mul_exp_le (w := w) hz hw0    have hew : (0:ℝ) ≤ exp (w ^ 2) := exp_nonneg _    calc (∫ u in (0:ℝ)..w, exp (u ^ 2 - 2 * z * u))        ≤ _ := hmono      _ = _ := hlin      _ ≤ 1 / (2 * z) + exp (w ^ 2) * (1 / (4 * z ^ 3)) := by          have := mul_le_mul_of_nonneg_left hsq hew          linarith      _ = 1 / (2 * z) + exp (w ^ 2) / (4 * z ^ 3) := by ring  have tail : (∫ u in w..z, exp (u ^ 2 - 2 * z * u)) ≤      (z - w) * exp (-(w * (2 * z - w))) := by    have hptw : ∀ u ∈ Set.Icc w z,        exp (u ^ 2 - 2 * z * u) ≤ exp (-(w * (2 * z - w))) := by      intro u hu      apply Real.exp_le_exp.mpr      nlinarith [hu.1, hu.2]    calc (∫ u in w..z, exp (u ^ 2 - 2 * z * u))        ≤ ∫ _u in w..z, exp (-(w * (2 * z - w))) :=          intervalIntegral.integral_mono_on hwz (hint w z)            _root_.intervalIntegrable_const hptw      _ = (z - w) * exp (-(w * (2 * z - w))) := by          rw [intervalIntegral.integral_const]          ring  linarith [head, tail]