English
The map c -> ∫_{-∞}^{∞} exp(-c x^2) dx is continuous at every point with Re(c) > 0.
Русский
Пусть Re(c) > 0. Карта c ↦ ∫_{-∞}^{∞} exp(-c x^2) dx непрерывна в c.
LaTeX
$$$$\\text{ContinuousAt}\\left(c \\mapsto \\int_{-\\infty}^{\\infty} e^{-c x^2}\\, dx\\right)\\; b,$$$$
Lean4
theorem continuousAt_gaussian_integral (b : ℂ) (hb : 0 < re b) :
ContinuousAt (fun c : ℂ => ∫ x : ℝ, cexp (-c * (x : ℂ) ^ 2)) b :=
by
let f : ℂ → ℝ → ℂ := fun (c : ℂ) (x : ℝ) => cexp (-c * (x : ℂ) ^ 2)
obtain ⟨d, hd, hd'⟩ := exists_between hb
have f_meas : ∀ c : ℂ, AEStronglyMeasurable (f c) volume := fun c =>
by
apply Continuous.aestronglyMeasurable
exact Complex.continuous_exp.comp (continuous_const.mul (continuous_ofReal.pow 2))
have f_cts : ∀ x : ℝ, ContinuousAt (fun c => f c x) b := fun x =>
(Complex.continuous_exp.comp (continuous_id'.neg.mul continuous_const)).continuousAt
have f_le_bd : ∀ᶠ c : ℂ in 𝓝 b, ∀ᵐ x : ℝ, ‖f c x‖ ≤ exp (-d * x ^ 2) :=
by
refine eventually_of_mem ((continuous_re.isOpen_preimage _ isOpen_Ioi).mem_nhds hd') ?_
intro c hc; filter_upwards with x
rw [norm_cexp_neg_mul_sq]
gcongr
exact le_of_lt hc
exact
continuousAt_of_dominated (Eventually.of_forall f_meas) f_le_bd (integrable_exp_neg_mul_sq hd) (ae_of_all _ f_cts)
