Source indexedlemma · leanprover/lean4:v4.32.0

FKS2.dawson_eq_integral

PrimeNumberTheoremAnd.IEANTN.FKS2 · PrimeNumberTheoremAnd/IEANTN/FKS2.lean:306 to 320

Source documentation

Substituted form: dawson z = ∫₀^z exp (u² − 2zu) du.

Exact Lean statement

lemma dawson_eq_integral (z : ℝ) :
    dawson z = ∫ u in (0:ℝ)..z, exp (u ^ 2 - 2 * z * u)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma dawson_eq_integral (z : ℝ) :    dawson z = ∫ u in (0:ℝ)..z, exp (u ^ 2 - 2 * z * u) := by  unfold dawson  have hsub : (∫ t in (0:ℝ)..z, exp (t ^ 2)) =      ∫ u in (0:ℝ)..z, exp ((z - u) ^ 2) := by    have := intervalIntegral.integral_comp_sub_left (a := (0:ℝ)) (b := z)      (fun t => exp (t ^ 2)) z    simpa using this.symm  rw [hsub, ← intervalIntegral.integral_const_mul]  apply intervalIntegral.integral_congr  intro u _  change exp (-z ^ 2) * exp ((z - u) ^ 2) = exp (u ^ 2 - 2 * z * u)  rw [← Real.exp_add]  congr 1  ring