-- Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean
theorem integral_gaussian_sq_complex {b : ℂ} (hb : 0 < b.re) :
    (∫ x : ℝ, cexp (-b * (x : ℂ) ^ 2)) ^ 2 = π / b

Proof state:
b : ℂ
hb : 0 < b.re
⊢ ∫ (p : ℝ × ℝ), cexp (-b * (↑p.1 ^ 2 + ↑p.2 ^ 2)) =
    ∫ (p : ℝ × ℝ) in polarCoord.target,
      p.1 • cexp (-b * ((↑p.1 * Complex.cos ↑p.2) ^ 2 + (↑p.1 * Complex.sin ↑p.2) ^ 2))

Tactic:
rw [← integral_comp_polarCoord_symm]

Result:
b : ℂ
hb : 0 < b.re
⊢ ∫ (p : ℝ × ℝ) in polarCoord.target, p.1 • cexp (-b * (↑(↑polarCoord.symm p).1 ^ 2 + ↑(↑polarCoord.symm p).2 ^ 2)) =
    ∫ (p : ℝ × ℝ) in polarCoord.target,
      p.1 • cexp (-b * ((↑p.1 * Complex.cos ↑p.2) ^ 2 + (↑p.1 * Complex.sin ↑p.2) ^ 2))

Proof state:
case e_f.h.e_a.e_z.e_a
b : ℂ
hb : 0 < b.re
p : ℝ × ℝ
⊢ (↑p.1 * Complex.cos ↑p.2) ^ 2 + (↑p.1 * Complex.sin ↑p.2) ^ 2 =
    (Complex.sin ↑p.2 ^ 2 + Complex.cos ↑p.2 ^ 2) * ↑p.1 ^ 2

Tactic:
ring

Result:
no goals

Proof state:
b : ℂ
hb : 0 < b.re
⊢ ∫ (p : ℝ × ℝ) in polarCoord.target,
      p.1 • cexp (-b * ((↑p.1 * Complex.cos ↑p.2) ^ 2 + (↑p.1 * Complex.sin ↑p.2) ^ 2)) =
    (∫ (r : ℝ) in Ioi 0, ↑r * cexp (-b * ↑r ^ 2)) * ∫ (θ : ℝ) in Ioo (-π) π, 1

Tactic:
rw [← setIntegral_prod_mul]

Result:
b : ℂ
hb : 0 < b.re
⊢ ∫ (p : ℝ × ℝ) in polarCoord.target,
      p.1 • cexp (-b * ((↑p.1 * Complex.cos ↑p.2) ^ 2 + (↑p.1 * Complex.sin ↑p.2) ^ 2)) =
    ∫ (z : ℝ × ℝ) in Ioi 0 ×ˢ Ioo (-π) π, ↑z.1 * cexp (-b * ↑z.1 ^ 2) * 1 ∂volume.prod volume

Proof state:
case e_f
b : ℂ
hb : 0 < b.re
⊢ (fun p => cexp (-b * ↑p.1 ^ 2) * cexp (-b * ↑p.2 ^ 2)) = fun p => cexp (-b * (↑p.1 ^ 2 + ↑p.2 ^ 2))

Tactic:
ext1 p

Result:
case e_f.h
b : ℂ
hb : 0 < b.re
p : ℝ × ℝ
⊢ cexp (-b * ↑p.1 ^ 2) * cexp (-b * ↑p.2 ^ 2) = cexp (-b * (↑p.1 ^ 2 + ↑p.2 ^ 2))

Proof state:
case e_f.h.e_a.e_z.e_a
b : ℂ
hb : 0 < b.re
p : ℝ × ℝ
⊢ (↑p.1 * Complex.cos ↑p.2) ^ 2 + (↑p.1 * Complex.sin ↑p.2) ^ 2 = ↑p.1 ^ 2

Tactic:
conv_rhs => rw [← one_mul ((p.1 : ℂ) ^ 2), ← sin_sq_add_cos_sq (p.2 : ℂ)]

Result:
case e_f.h.e_a.e_z.e_a
b : ℂ
hb : 0 < b.re
p : ℝ × ℝ
⊢ (↑p.1 * Complex.cos ↑p.2) ^ 2 + (↑p.1 * Complex.sin ↑p.2) ^ 2 =
    (Complex.sin ↑p.2 ^ 2 + Complex.cos ↑p.2 ^ 2) * ↑p.1 ^ 2

Proof state:
b : ℂ
hb : 0 < b.re
⊢ ∫ (p : ℝ × ℝ) in polarCoord.target, p.1 • cexp (-b * (↑(↑polarCoord.symm p).1 ^ 2 + ↑(↑polarCoord.symm p).2 ^ 2)) =
    ∫ (p : ℝ × ℝ) in polarCoord.target,
      p.1 • cexp (-b * ((↑p.1 * Complex.cos ↑p.2) ^ 2 + (↑p.1 * Complex.sin ↑p.2) ^ 2))

Tactic:
simp only [polarCoord_symm_apply, ofReal_mul, ofReal_cos, ofReal_sin]

Result:
no goals

Proof state:
b : ℂ
hb : 0 < b.re
this : 0 ≤ π + π
⊢ (∫ (r : ℝ) in Ioi 0, ↑r * cexp (-b * ↑r ^ 2)) * ∫ (θ : ℝ) in Ioo (-π) π, 1 = ↑π / b

Tactic:
simp only [integral_const, Measure.restrict_apply', measurableSet_Ioo, univ_inter, volume_Ioo,
  sub_neg_eq_add, ENNReal.toReal_ofReal, this]

Result:
b : ℂ
hb : 0 < b.re
this : 0 ≤ π + π
⊢ (∫ (r : ℝ) in Ioi 0, ↑r * cexp (-b * ↑r ^ 2)) * (π + π) • 1 = ↑π / b

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

Tactic:
calc
  (∫ x : ℝ, cexp (-b * (x : ℂ) ^ 2)) ^ 2 =
      ∫ p : ℝ × ℝ, cexp (-b * (p.1 : ℂ) ^ 2) * cexp (-b * (p.2 : ℂ) ^ 2) := by
    rw [pow_two, ← integral_prod_mul]; rfl
  _ = ∫ p : ℝ × ℝ, cexp (-b * ((p.1 : ℂ)^ 2 + (p.2 : ℂ) ^ 2)) := by
    congr
    ext1 p
    rw [← Complex.exp_add, mul_add]
  _ = ∫ p in polarCoord.target, p.1 •
      cexp (-b * ((p.1 * Complex.cos p.2) ^ 2 + (p.1 * Complex.sin p.2) ^ 2)) := by
    rw [← integral_comp_polarCoord_symm]
    simp only [polarCoord_symm_apply, ofReal_mul, ofReal_cos, ofReal_sin]
  _ = (∫ r in Ioi (0 : ℝ), r * cexp (-b * (r : ℂ) ^ 2)) * ∫ θ in Ioo (-π) π, 1 := by
    rw [← setIntegral_prod_mul]
    congr with p : 1
    rw [mul_one]
    congr
    conv_rhs => rw [← one_mul ((p.1 : ℂ) ^ 2), ← sin_sq_add_cos_sq (p.2 : ℂ)]
    ring
  _ = ↑π / b := by
    have : 0 ≤ π + π := by positivity
    simp only [integral_const, Measure.restrict_apply', measurableSet_Ioo, univ_inter, volume_Ioo,
      sub_neg_eq_add, ENNReal.toReal_ofReal, this]
    rw [← two_mul, real_smul, mul_one, ofReal_mul, ofReal_ofNat, integral_mul_cexp_neg_mul_sq hb]
    field_simp [(by contrapose! hb; rw [hb, zero_re] : b ≠ 0)]
    ring

Result:
no goals

Proof state:
case e_f.h
b : ℂ
hb : 0 < b.re
p : ℝ × ℝ
⊢ p.1 • cexp (-b * ((↑p.1 * Complex.cos ↑p.2) ^ 2 + (↑p.1 * Complex.sin ↑p.2) ^ 2)) = ↑p.1 * cexp (-b * ↑p.1 ^ 2) * 1

Tactic:
rw [mul_one]

Result:
case e_f.h
b : ℂ
hb : 0 < b.re
p : ℝ × ℝ
⊢ p.1 • cexp (-b * ((↑p.1 * Complex.cos ↑p.2) ^ 2 + (↑p.1 * Complex.sin ↑p.2) ^ 2)) = ↑p.1 * cexp (-b * ↑p.1 ^ 2)

Proof state:
b : ℂ
hb : 0 < b.re
⊢ (∫ (r : ℝ) in Ioi 0, ↑r * cexp (-b * ↑r ^ 2)) * ∫ (θ : ℝ) in Ioo (-π) π, 1 = ↑π / b

Tactic:
have : 0 ≤ π + π := by positivity

Result:
b : ℂ
hb : 0 < b.re
this : 0 ≤ π + π
⊢ (∫ (r : ℝ) in Ioi 0, ↑r * cexp (-b * ↑r ^ 2)) * ∫ (θ : ℝ) in Ioo (-π) π, 1 = ↑π / b

Proof state:
b : ℂ
hb : 0 < b.re
⊢ ∫ (z : ℝ × ℝ), cexp (-b * ↑z.1 ^ 2) * cexp (-b * ↑z.2 ^ 2) ∂volume.prod volume =
    ∫ (p : ℝ × ℝ), cexp (-b * ↑p.1 ^ 2) * cexp (-b * ↑p.2 ^ 2)

Tactic:
rfl

Result:
no goals

Proof state:
b : ℂ
hb : 0 < b.re
this : 0 ≤ π + π
⊢ (2 * b)⁻¹ * (2 * ↑π) = ↑π / b

Tactic:
field_simp [(by contrapose! hb; rw [hb, zero_re] : b ≠ 0)]

Result:
b : ℂ
hb : 0 < b.re
this : 0 ≤ π + π
⊢ 2 * ↑π * b = ↑π * (2 * b)

Proof state:
case e_f.h
b : ℂ
hb : 0 < b.re
p : ℝ × ℝ
⊢ cexp (-b * ↑p.1 ^ 2) * cexp (-b * ↑p.2 ^ 2) = cexp (-b * (↑p.1 ^ 2 + ↑p.2 ^ 2))

Tactic:
rw [← Complex.exp_add, mul_add]

Result:
no goals

Proof state:
b : ℂ
hb : 0 < b.re
this : 0 ≤ π + π
⊢ b ≠ 0

Tactic:
contrapose! hb

Result:
b : ℂ
this : 0 ≤ π + π
hb : b = 0
⊢ b.re ≤ 0

Proof state:
b : ℂ
hb : 0 < b.re
⊢ ∫ (p : ℝ × ℝ), cexp (-b * ↑p.1 ^ 2) * cexp (-b * ↑p.2 ^ 2) = ∫ (p : ℝ × ℝ), cexp (-b * (↑p.1 ^ 2 + ↑p.2 ^ 2))

Tactic:
congr

Result:
case e_f
b : ℂ
hb : 0 < b.re
⊢ (fun p => cexp (-b * ↑p.1 ^ 2) * cexp (-b * ↑p.2 ^ 2)) = fun p => cexp (-b * (↑p.1 ^ 2 + ↑p.2 ^ 2))

Proof state:
b : ℂ
hb : 0 < b.re
this : 0 ≤ π + π
⊢ (∫ (r : ℝ) in Ioi 0, ↑r * cexp (-b * ↑r ^ 2)) * (π + π) • 1 = ↑π / b

Tactic:
rw [← two_mul, real_smul, mul_one, ofReal_mul, ofReal_ofNat, integral_mul_cexp_neg_mul_sq hb]

Result:
b : ℂ
hb : 0 < b.re
this : 0 ≤ π + π
⊢ (2 * b)⁻¹ * (2 * ↑π) = ↑π / b

Proof state:
b : ℂ
this : 0 ≤ π + π
hb : b = 0
⊢ b.re ≤ 0

Tactic:
rw [hb, zero_re]

Result:
no goals

Proof state:
b : ℂ
hb : 0 < b.re
⊢ ∫ (p : ℝ × ℝ) in polarCoord.target,
      p.1 • cexp (-b * ((↑p.1 * Complex.cos ↑p.2) ^ 2 + (↑p.1 * Complex.sin ↑p.2) ^ 2)) =
    ∫ (z : ℝ × ℝ) in Ioi 0 ×ˢ Ioo (-π) π, ↑z.1 * cexp (-b * ↑z.1 ^ 2) * 1 ∂volume.prod volume

Tactic:
congr with p : 1

Result:
case e_f.h
b : ℂ
hb : 0 < b.re
p : ℝ × ℝ
⊢ p.1 • cexp (-b * ((↑p.1 * Complex.cos ↑p.2) ^ 2 + (↑p.1 * Complex.sin ↑p.2) ^ 2)) = ↑p.1 * cexp (-b * ↑p.1 ^ 2) * 1

Proof state:
case e_f.h
b : ℂ
hb : 0 < b.re
p : ℝ × ℝ
⊢ p.1 • cexp (-b * ((↑p.1 * Complex.cos ↑p.2) ^ 2 + (↑p.1 * Complex.sin ↑p.2) ^ 2)) = ↑p.1 * cexp (-b * ↑p.1 ^ 2)

Tactic:
congr

Result:
case e_f.h.e_a.e_z.e_a
b : ℂ
hb : 0 < b.re
p : ℝ × ℝ
⊢ (↑p.1 * Complex.cos ↑p.2) ^ 2 + (↑p.1 * Complex.sin ↑p.2) ^ 2 = ↑p.1 ^ 2

Proof state:
b : ℂ
hb : 0 < b.re
⊢ 0 ≤ π + π

Tactic:
positivity

Result:
no goals

Proof state:
b : ℂ
hb : 0 < b.re
⊢ (∫ (x : ℝ), cexp (-b * ↑x ^ 2)) ^ 2 = ∫ (p : ℝ × ℝ), cexp (-b * ↑p.1 ^ 2) * cexp (-b * ↑p.2 ^ 2)

Tactic:
rw [pow_two, ← integral_prod_mul]

Result:
b : ℂ
hb : 0 < b.re
⊢ ∫ (z : ℝ × ℝ), cexp (-b * ↑z.1 ^ 2) * cexp (-b * ↑z.2 ^ 2) ∂volume.prod volume =
    ∫ (p : ℝ × ℝ), cexp (-b * ↑p.1 ^ 2) * cexp (-b * ↑p.2 ^ 2)

Proof state:
b : ℂ
hb : 0 < b.re
this : 0 ≤ π + π
⊢ 2 * ↑π * b = ↑π * (2 * b)

Tactic:
ring

Result:
no goals