-- Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean
theorem continuousAt_gaussian_integral (b : ℂ) (hb : 0 < re b) :
    ContinuousAt (fun c : ℂ => ∫ x : ℝ, cexp (-c * (x : ℂ) ^ 2)) b

Proof state:
case hf
b : ℂ
hb : 0 < b.re
f : ℂ → ℝ → ℂ := fun c x => cexp (-c * ↑x ^ 2)
d : ℝ
hd : 0 < d
hd' : d < b.re
c : ℂ
⊢ Continuous (f c)

Tactic:
exact Complex.continuous_exp.comp (continuous_const.mul (continuous_ofReal.pow 2))

Result:
no goals

Proof state:
case intro.intro
b : ℂ
hb : 0 < b.re
f : ℂ → ℝ → ℂ := fun c x => cexp (-c * ↑x ^ 2)
d : ℝ
hd : 0 < d
hd' : d < b.re
f_meas : ∀ (c : ℂ), AEStronglyMeasurable (f c) volume
f_cts : ∀ (x : ℝ), ContinuousAt (fun c => f c x) b
⊢ ContinuousAt (fun c => ∫ (x : ℝ), cexp (-c * ↑x ^ 2)) b

Tactic:
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

Result:
case intro.intro
b : ℂ
hb : 0 < b.re
f : ℂ → ℝ → ℂ := fun c x => cexp (-c * ↑x ^ 2)
d : ℝ
hd : 0 < d
hd' : d < b.re
f_meas : ∀ (c : ℂ), AEStronglyMeasurable (f c) volume
f_cts : ∀ (x : ℝ), ContinuousAt (fun c => f c x) b
f_le_bd : ∀ᶠ (c : ℂ) in 𝓝 b, ∀ᵐ (x : ℝ), ‖f c x‖ ≤ rexp (-d * x ^ 2)
⊢ ContinuousAt (fun c => ∫ (x : ℝ), cexp (-c * ↑x ^ 2)) b

Proof state:
b : ℂ
hb : 0 < b.re
f : ℂ → ℝ → ℂ := fun c x => cexp (-c * ↑x ^ 2)
d : ℝ
hd : 0 < d
hd' : d < b.re
c : ℂ
⊢ AEStronglyMeasurable (f c) volume

Tactic:
apply Continuous.aestronglyMeasurable

Result:
case hf
b : ℂ
hb : 0 < b.re
f : ℂ → ℝ → ℂ := fun c x => cexp (-c * ↑x ^ 2)
d : ℝ
hd : 0 < d
hd' : d < b.re
c : ℂ
⊢ Continuous (f c)

Proof state:
case h.h.h.a
b : ℂ
hb : 0 < b.re
f : ℂ → ℝ → ℂ := fun c x => cexp (-c * ↑x ^ 2)
d : ℝ
hd : 0 < d
hd' : d < b.re
f_meas : ∀ (c : ℂ), AEStronglyMeasurable (f c) volume
f_cts : ∀ (x : ℝ), ContinuousAt (fun c => f c x) b
c : ℂ
hc : c ∈ re ⁻¹' Ioi d
x : ℝ
⊢ d ≤ c.re

Tactic:
exact le_of_lt hc

Result:
no goals

Proof state:
b : ℂ
hb : 0 < b.re
f : ℂ → ℝ → ℂ := fun c x => cexp (-c * ↑x ^ 2)
⊢ ContinuousAt (fun c => ∫ (x : ℝ), cexp (-c * ↑x ^ 2)) b

Tactic:
obtain ⟨d, hd, hd'⟩ := exists_between hb

Result:
case intro.intro
b : ℂ
hb : 0 < b.re
f : ℂ → ℝ → ℂ := fun c x => cexp (-c * ↑x ^ 2)
d : ℝ
hd : 0 < d
hd' : d < b.re
⊢ ContinuousAt (fun c => ∫ (x : ℝ), cexp (-c * ↑x ^ 2)) b

Proof state:
case intro.intro
b : ℂ
hb : 0 < b.re
f : ℂ → ℝ → ℂ := fun c x => cexp (-c * ↑x ^ 2)
d : ℝ
hd : 0 < d
hd' : d < b.re
f_meas : ∀ (c : ℂ), AEStronglyMeasurable (f c) volume
⊢ ContinuousAt (fun c => ∫ (x : ℝ), cexp (-c * ↑x ^ 2)) b

Tactic:
have f_cts : ∀ x : ℝ, ContinuousAt (fun c => f c x) b := fun x =>
  (Complex.continuous_exp.comp (continuous_id'.neg.mul continuous_const)).continuousAt

Result:
case intro.intro
b : ℂ
hb : 0 < b.re
f : ℂ → ℝ → ℂ := fun c x => cexp (-c * ↑x ^ 2)
d : ℝ
hd : 0 < d
hd' : d < b.re
f_meas : ∀ (c : ℂ), AEStronglyMeasurable (f c) volume
f_cts : ∀ (x : ℝ), ContinuousAt (fun c => f c x) b
⊢ ContinuousAt (fun c => ∫ (x : ℝ), cexp (-c * ↑x ^ 2)) b

Proof state:
case intro.intro
b : ℂ
hb : 0 < b.re
f : ℂ → ℝ → ℂ := fun c x => cexp (-c * ↑x ^ 2)
d : ℝ
hd : 0 < d
hd' : d < b.re
f_meas : ∀ (c : ℂ), AEStronglyMeasurable (f c) volume
f_cts : ∀ (x : ℝ), ContinuousAt (fun c => f c x) b
f_le_bd : ∀ᶠ (c : ℂ) in 𝓝 b, ∀ᵐ (x : ℝ), ‖f c x‖ ≤ rexp (-d * x ^ 2)
⊢ ContinuousAt (fun c => ∫ (x : ℝ), cexp (-c * ↑x ^ 2)) b

Tactic:
exact
  continuousAt_of_dominated (Eventually.of_forall f_meas) f_le_bd (integrable_exp_neg_mul_sq hd)
    (ae_of_all _ f_cts)

Result:
no goals

Proof state:
case h
b : ℂ
hb : 0 < b.re
f : ℂ → ℝ → ℂ := fun c x => cexp (-c * ↑x ^ 2)
d : ℝ
hd : 0 < d
hd' : d < b.re
f_meas : ∀ (c : ℂ), AEStronglyMeasurable (f c) volume
f_cts : ∀ (x : ℝ), ContinuousAt (fun c => f c x) b
c : ℂ
hc : c ∈ re ⁻¹' Ioi d
x : ℝ
⊢ ‖f c x‖ ≤ rexp (-d * x ^ 2)

Tactic:
rw [norm_cexp_neg_mul_sq]

Result:
case h
b : ℂ
hb : 0 < b.re
f : ℂ → ℝ → ℂ := fun c x => cexp (-c * ↑x ^ 2)
d : ℝ
hd : 0 < d
hd' : d < b.re
f_meas : ∀ (c : ℂ), AEStronglyMeasurable (f c) volume
f_cts : ∀ (x : ℝ), ContinuousAt (fun c => f c x) b
c : ℂ
hc : c ∈ re ⁻¹' Ioi d
x : ℝ
⊢ rexp (-c.re * x ^ 2) ≤ rexp (-d * x ^ 2)

Proof state:
b : ℂ
hb : 0 < b.re
f : ℂ → ℝ → ℂ := fun c x => cexp (-c * ↑x ^ 2)
d : ℝ
hd : 0 < d
hd' : d < b.re
f_meas : ∀ (c : ℂ), AEStronglyMeasurable (f c) volume
f_cts : ∀ (x : ℝ), ContinuousAt (fun c => f c x) b
⊢ ∀ x ∈ re ⁻¹' Ioi d, ∀ᵐ (x_1 : ℝ), ‖f x x_1‖ ≤ rexp (-d * x_1 ^ 2)

Tactic:
intro c hc

Result:
b : ℂ
hb : 0 < b.re
f : ℂ → ℝ → ℂ := fun c x => cexp (-c * ↑x ^ 2)
d : ℝ
hd : 0 < d
hd' : d < b.re
f_meas : ∀ (c : ℂ), AEStronglyMeasurable (f c) volume
f_cts : ∀ (x : ℝ), ContinuousAt (fun c => f c x) b
c : ℂ
hc : c ∈ re ⁻¹' Ioi d
⊢ ∀ᵐ (x : ℝ), ‖f c x‖ ≤ rexp (-d * x ^ 2)

Proof state:
b : ℂ
hb : 0 < b.re
⊢ ContinuousAt (fun c => ∫ (x : ℝ), cexp (-c * ↑x ^ 2)) b

Tactic:
let f : ℂ → ℝ → ℂ := fun (c : ℂ) (x : ℝ) => cexp (-c * (x : ℂ) ^ 2)

Result:
b : ℂ
hb : 0 < b.re
f : ℂ → ℝ → ℂ := fun c x => cexp (-c * ↑x ^ 2)
⊢ ContinuousAt (fun c => ∫ (x : ℝ), cexp (-c * ↑x ^ 2)) b

Proof state:
b : ℂ
hb : 0 < b.re
f : ℂ → ℝ → ℂ := fun c x => cexp (-c * ↑x ^ 2)
d : ℝ
hd : 0 < d
hd' : d < b.re
f_meas : ∀ (c : ℂ), AEStronglyMeasurable (f c) volume
f_cts : ∀ (x : ℝ), ContinuousAt (fun c => f c x) b
⊢ ∀ᶠ (c : ℂ) in 𝓝 b, ∀ᵐ (x : ℝ), ‖f c x‖ ≤ rexp (-d * x ^ 2)

Tactic:
refine eventually_of_mem ((continuous_re.isOpen_preimage _ isOpen_Ioi).mem_nhds hd') ?_

Result:
b : ℂ
hb : 0 < b.re
f : ℂ → ℝ → ℂ := fun c x => cexp (-c * ↑x ^ 2)
d : ℝ
hd : 0 < d
hd' : d < b.re
f_meas : ∀ (c : ℂ), AEStronglyMeasurable (f c) volume
f_cts : ∀ (x : ℝ), ContinuousAt (fun c => f c x) b
⊢ ∀ x ∈ re ⁻¹' Ioi d, ∀ᵐ (x_1 : ℝ), ‖f x x_1‖ ≤ rexp (-d * x_1 ^ 2)

Proof state:
case intro.intro
b : ℂ
hb : 0 < b.re
f : ℂ → ℝ → ℂ := fun c x => cexp (-c * ↑x ^ 2)
d : ℝ
hd : 0 < d
hd' : d < b.re
⊢ ContinuousAt (fun c => ∫ (x : ℝ), cexp (-c * ↑x ^ 2)) b

Tactic:
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))

Result:
case intro.intro
b : ℂ
hb : 0 < b.re
f : ℂ → ℝ → ℂ := fun c x => cexp (-c * ↑x ^ 2)
d : ℝ
hd : 0 < d
hd' : d < b.re
f_meas : ∀ (c : ℂ), AEStronglyMeasurable (f c) volume
⊢ ContinuousAt (fun c => ∫ (x : ℝ), cexp (-c * ↑x ^ 2)) b

Proof state:
b : ℂ
hb : 0 < b.re
f : ℂ → ℝ → ℂ := fun c x => cexp (-c * ↑x ^ 2)
d : ℝ
hd : 0 < d
hd' : d < b.re
f_meas : ∀ (c : ℂ), AEStronglyMeasurable (f c) volume
f_cts : ∀ (x : ℝ), ContinuousAt (fun c => f c x) b
c : ℂ
hc : c ∈ re ⁻¹' Ioi d
⊢ ∀ᵐ (x : ℝ), ‖f c x‖ ≤ rexp (-d * x ^ 2)

Tactic:
filter_upwards with x

Result:
case h
b : ℂ
hb : 0 < b.re
f : ℂ → ℝ → ℂ := fun c x => cexp (-c * ↑x ^ 2)
d : ℝ
hd : 0 < d
hd' : d < b.re
f_meas : ∀ (c : ℂ), AEStronglyMeasurable (f c) volume
f_cts : ∀ (x : ℝ), ContinuousAt (fun c => f c x) b
c : ℂ
hc : c ∈ re ⁻¹' Ioi d
x : ℝ
⊢ ‖f c x‖ ≤ rexp (-d * x ^ 2)

Proof state:
case h
b : ℂ
hb : 0 < b.re
f : ℂ → ℝ → ℂ := fun c x => cexp (-c * ↑x ^ 2)
d : ℝ
hd : 0 < d
hd' : d < b.re
f_meas : ∀ (c : ℂ), AEStronglyMeasurable (f c) volume
f_cts : ∀ (x : ℝ), ContinuousAt (fun c => f c x) b
c : ℂ
hc : c ∈ re ⁻¹' Ioi d
x : ℝ
⊢ rexp (-c.re * x ^ 2) ≤ rexp (-d * x ^ 2)

Tactic:
gcongr

Result:
case h.h.h.a
b : ℂ
hb : 0 < b.re
f : ℂ → ℝ → ℂ := fun c x => cexp (-c * ↑x ^ 2)
d : ℝ
hd : 0 < d
hd' : d < b.re
f_meas : ∀ (c : ℂ), AEStronglyMeasurable (f c) volume
f_cts : ∀ (x : ℝ), ContinuousAt (fun c => f c x) b
c : ℂ
hc : c ∈ re ⁻¹' Ioi d
x : ℝ
⊢ d ≤ c.re