-- Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean
theorem _root_.fourierIntegral_gaussian_pi' (hb : 0 < b.re) (c : ℂ) :
    (𝓕 fun x : ℝ => cexp (-π * b * x ^ 2 + 2 * π * c * x)) = fun t : ℝ =>
    1 / b ^ (1 / 2 : ℂ) * cexp (-π / b * (t + I * c) ^ 2)

Proof state:
b : ℂ
hb : 0 < b.re
c : ℂ
this : b ≠ 0
⊢ (-↑π * b).re < 0

Tactic:
simpa only [neg_mul, neg_re, re_ofReal_mul, neg_lt_zero] using mul_pos pi_pos hb

Result:
no goals

Proof state:
b : ℂ
hb : 0 < b.re
c : ℂ
this : b ≠ 0
h : (-↑π * b).re < 0
t x : ℝ
⊢ ↑(-2 * π * x * t) * I + -↑π * b * ↑x ^ 2 + 2 * ↑π * c * ↑x =
    -↑π * b * ↑x ^ 2 + (-2 * ↑π * I * ↑t + 2 * ↑π * c) * ↑x + 0

Tactic:
push_cast

Result:
b : ℂ
hb : 0 < b.re
c : ℂ
this : b ≠ 0
h : (-↑π * b).re < 0
t x : ℝ
⊢ -2 * ↑π * ↑x * ↑t * I + -↑π * b * ↑x ^ 2 + 2 * ↑π * c * ↑x =
    -↑π * b * ↑x ^ 2 + (-2 * ↑π * I * ↑t + 2 * ↑π * c) * ↑x + 0

Proof state:
case h.e_a.e_z
b : ℂ
hb : 0 < b.re
c : ℂ
this✝ : b ≠ 0
h : (-↑π * b).re < 0
t : ℝ
this :
  ∀ (x : ℝ),
    ↑(-2 * π * x * t) * I + -↑π * b * ↑x ^ 2 + 2 * ↑π * c * ↑x =
      -↑π * b * ↑x ^ 2 + (-2 * ↑π * I * ↑t + 2 * ↑π * c) * ↑x + 0
⊢ 0 - (-(2 * ↑π * I * ↑t) + 2 * ↑π * c) ^ 2 / (4 * -(↑π * b)) = -↑π / b * (↑t + I * c) ^ 2

Tactic:
field_simp [ofReal_ne_zero.mpr pi_ne_zero]

Result:
case h.e_a.e_z
b : ℂ
hb : 0 < b.re
c : ℂ
this✝ : b ≠ 0
h : (-↑π * b).re < 0
t : ℝ
this :
  ∀ (x : ℝ),
    ↑(-2 * π * x * t) * I + -↑π * b * ↑x ^ 2 + 2 * ↑π * c * ↑x =
      -↑π * b * ↑x ^ 2 + (-2 * ↑π * I * ↑t + 2 * ↑π * c) * ↑x + 0
⊢ (-(2 * ↑π * I * ↑t) + 2 * ↑π * c) ^ 2 * b = -(↑π * (↑t + I * c) ^ 2 * (4 * (↑π * b)))

Proof state:
b : ℂ
hb : 0 < b.re
c : ℂ
this : b ≠ 0
h : (-↑π * b).re < 0
t x : ℝ
⊢ -2 * ↑π * ↑x * ↑t * I + -↑π * b * ↑x ^ 2 + 2 * ↑π * c * ↑x =
    -↑π * b * ↑x ^ 2 + (-2 * ↑π * I * ↑t + 2 * ↑π * c) * ↑x + 0

Tactic:
ring

Result:
no goals

Proof state:
case h
b : ℂ
hb : 0 < b.re
c : ℂ
this : b ≠ 0
h : (-↑π * b).re < 0
t : ℝ
⊢ 𝓕 (fun x => cexp (-↑π * b * ↑x ^ 2 + 2 * ↑π * c * ↑x)) t = 1 / b ^ (1 / 2) * cexp (-↑π / b * (↑t + I * c) ^ 2)

Tactic:
simp_rw [fourierIntegral_real_eq_integral_exp_smul, smul_eq_mul, ← Complex.exp_add, ← add_assoc]

Result:
case h
b : ℂ
hb : 0 < b.re
c : ℂ
this : b ≠ 0
h : (-↑π * b).re < 0
t : ℝ
⊢ ∫ (v : ℝ), cexp (↑(-2 * π * v * t) * I + -↑π * b * ↑v ^ 2 + 2 * ↑π * c * ↑v) =
    1 / b ^ (1 / 2) * cexp (-↑π / b * (↑t + I * c) ^ 2)

Proof state:
case h.e_a.e_z
b : ℂ
hb : 0 < b.re
c : ℂ
this✝ : b ≠ 0
h : (-↑π * b).re < 0
t : ℝ
this :
  ∀ (x : ℝ),
    ↑(-2 * π * x * t) * I + -↑π * b * ↑x ^ 2 + 2 * ↑π * c * ↑x =
      -↑π * b * ↑x ^ 2 + (-2 * ↑π * I * ↑t + 2 * ↑π * c) * ↑x + 0
⊢ -(↑π ^ 2 * I * ↑t * c * b * 8) + ↑π ^ 2 * -1 * ↑t ^ 2 * b * 4 + ↑π ^ 2 * c ^ 2 * b * 4 =
    -(↑π ^ 2 * I * ↑t * c * b * 8) + (-(↑π ^ 2 * -1 * c ^ 2 * b * 4) - ↑π ^ 2 * ↑t ^ 2 * b * 4)

Tactic:
ring

Result:
no goals

Proof state:
b c : ℂ
hb : b = 0
⊢ b.re ≤ 0

Tactic:
rw [hb, zero_re]

Result:
no goals

Proof state:
b : ℂ
hb : 0 < b.re
c : ℂ
this : b ≠ 0
⊢ (𝓕 fun x => cexp (-↑π * b * ↑x ^ 2 + 2 * ↑π * c * ↑x)) = fun t => 1 / b ^ (1 / 2) * cexp (-↑π / b * (↑t + I * c) ^ 2)

Tactic:
have h : (-↑π * b).re < 0 := by
  simpa only [neg_mul, neg_re, re_ofReal_mul, neg_lt_zero] using mul_pos pi_pos hb

Result:
b : ℂ
hb : 0 < b.re
c : ℂ
this : b ≠ 0
h : (-↑π * b).re < 0
⊢ (𝓕 fun x => cexp (-↑π * b * ↑x ^ 2 + 2 * ↑π * c * ↑x)) = fun t => 1 / b ^ (1 / 2) * cexp (-↑π / b * (↑t + I * c) ^ 2)

Proof state:
case h.e_a
b : ℂ
hb : 0 < b.re
c : ℂ
this✝ : b ≠ 0
h : (-↑π * b).re < 0
t : ℝ
this :
  ∀ (x : ℝ),
    ↑(-2 * π * x * t) * I + -↑π * b * ↑x ^ 2 + 2 * ↑π * c * ↑x =
      -↑π * b * ↑x ^ 2 + (-2 * ↑π * I * ↑t + 2 * ↑π * c) * ↑x + 0
⊢ (↑π / (↑π * b)) ^ (1 / 2) = 1 / b ^ (1 / 2)

Tactic:
rw [← div_div, div_self <| ofReal_ne_zero.mpr pi_ne_zero, one_div, inv_cpow, ← one_div]

Result:
case h.e_a.hx
b : ℂ
hb : 0 < b.re
c : ℂ
this✝ : b ≠ 0
h : (-↑π * b).re < 0
t : ℝ
this :
  ∀ (x : ℝ),
    ↑(-2 * π * x * t) * I + -↑π * b * ↑x ^ 2 + 2 * ↑π * c * ↑x =
      -↑π * b * ↑x ^ 2 + (-2 * ↑π * I * ↑t + 2 * ↑π * c) * ↑x + 0
⊢ b.arg ≠ π

Proof state:
case h.e_a.hx
b : ℂ
hb : 0 < b.re
c : ℂ
this✝ : b ≠ 0
h : (-↑π * b).re < 0
t : ℝ
this :
  ∀ (x : ℝ),
    ↑(-2 * π * x * t) * I + -↑π * b * ↑x ^ 2 + 2 * ↑π * c * ↑x =
      -↑π * b * ↑x ^ 2 + (-2 * ↑π * I * ↑t + 2 * ↑π * c) * ↑x + 0
⊢ b.arg ≠ π

Tactic:
rw [Ne, arg_eq_pi_iff, not_and_or, not_lt]

Result:
case h.e_a.hx
b : ℂ
hb : 0 < b.re
c : ℂ
this✝ : b ≠ 0
h : (-↑π * b).re < 0
t : ℝ
this :
  ∀ (x : ℝ),
    ↑(-2 * π * x * t) * I + -↑π * b * ↑x ^ 2 + 2 * ↑π * c * ↑x =
      -↑π * b * ↑x ^ 2 + (-2 * ↑π * I * ↑t + 2 * ↑π * c) * ↑x + 0
⊢ 0 ≤ b.re ∨ ¬b.im = 0

Proof state:
b : ℂ
hb : 0 < b.re
c : ℂ
this : b ≠ 0
h : (-↑π * b).re < 0
⊢ (𝓕 fun x => cexp (-↑π * b * ↑x ^ 2 + 2 * ↑π * c * ↑x)) = fun t => 1 / b ^ (1 / 2) * cexp (-↑π / b * (↑t + I * c) ^ 2)

Tactic:
ext1 t

Result:
case h
b : ℂ
hb : 0 < b.re
c : ℂ
this : b ≠ 0
h : (-↑π * b).re < 0
t : ℝ
⊢ 𝓕 (fun x => cexp (-↑π * b * ↑x ^ 2 + 2 * ↑π * c * ↑x)) t = 1 / b ^ (1 / 2) * cexp (-↑π / b * (↑t + I * c) ^ 2)

Proof state:
case h.e_a.e_z
b : ℂ
hb : 0 < b.re
c : ℂ
this✝ : b ≠ 0
h : (-↑π * b).re < 0
t : ℝ
this :
  ∀ (x : ℝ),
    ↑(-2 * π * x * t) * I + -↑π * b * ↑x ^ 2 + 2 * ↑π * c * ↑x =
      -↑π * b * ↑x ^ 2 + (-2 * ↑π * I * ↑t + 2 * ↑π * c) * ↑x + 0
⊢ -(↑π ^ 2 * I * ↑t * c * b * 8) + ↑π ^ 2 * I ^ 2 * ↑t ^ 2 * b * 4 + ↑π ^ 2 * c ^ 2 * b * 4 =
    -(↑π ^ 2 * I * ↑t * c * b * 8) + (-(↑π ^ 2 * I ^ 2 * c ^ 2 * b * 4) - ↑π ^ 2 * ↑t ^ 2 * b * 4)

Tactic:
simp only [I_sq]

Result:
case h.e_a.e_z
b : ℂ
hb : 0 < b.re
c : ℂ
this✝ : b ≠ 0
h : (-↑π * b).re < 0
t : ℝ
this :
  ∀ (x : ℝ),
    ↑(-2 * π * x * t) * I + -↑π * b * ↑x ^ 2 + 2 * ↑π * c * ↑x =
      -↑π * b * ↑x ^ 2 + (-2 * ↑π * I * ↑t + 2 * ↑π * c) * ↑x + 0
⊢ -(↑π ^ 2 * I * ↑t * c * b * 8) + ↑π ^ 2 * -1 * ↑t ^ 2 * b * 4 + ↑π ^ 2 * c ^ 2 * b * 4 =
    -(↑π ^ 2 * I * ↑t * c * b * 8) + (-(↑π ^ 2 * -1 * c ^ 2 * b * 4) - ↑π ^ 2 * ↑t ^ 2 * b * 4)

Proof state:
case h
b : ℂ
hb : 0 < b.re
c : ℂ
this : b ≠ 0
h : (-↑π * b).re < 0
t : ℝ
⊢ ∫ (v : ℝ), cexp (↑(-2 * π * v * t) * I + -↑π * b * ↑v ^ 2 + 2 * ↑π * c * ↑v) =
    1 / b ^ (1 / 2) * cexp (-↑π / b * (↑t + I * c) ^ 2)

Tactic:
have (x : ℝ) : ↑(-2 * π * x * t) * I + -π * b * x ^ 2 + 2 * π * c * x =
  -π * b * x ^ 2 + (-2 * π * I * t + 2 * π * c) * x + 0 := by push_cast; ring

Result:
case h
b : ℂ
hb : 0 < b.re
c : ℂ
this✝ : b ≠ 0
h : (-↑π * b).re < 0
t : ℝ
this :
  ∀ (x : ℝ),
    ↑(-2 * π * x * t) * I + -↑π * b * ↑x ^ 2 + 2 * ↑π * c * ↑x =
      -↑π * b * ↑x ^ 2 + (-2 * ↑π * I * ↑t + 2 * ↑π * c) * ↑x + 0
⊢ ∫ (v : ℝ), cexp (↑(-2 * π * v * t) * I + -↑π * b * ↑v ^ 2 + 2 * ↑π * c * ↑v) =
    1 / b ^ (1 / 2) * cexp (-↑π / b * (↑t + I * c) ^ 2)

Proof state:
case h.e_a.e_z
b : ℂ
hb : 0 < b.re
c : ℂ
this✝ : b ≠ 0
h : (-↑π * b).re < 0
t : ℝ
this :
  ∀ (x : ℝ),
    ↑(-2 * π * x * t) * I + -↑π * b * ↑x ^ 2 + 2 * ↑π * c * ↑x =
      -↑π * b * ↑x ^ 2 + (-2 * ↑π * I * ↑t + 2 * ↑π * c) * ↑x + 0
⊢ (-(2 * ↑π * I * ↑t) + 2 * ↑π * c) ^ 2 * b = -(↑π * (↑t + I * c) ^ 2 * (4 * (↑π * b)))

Tactic:
ring_nf

Result:
case h.e_a.e_z
b : ℂ
hb : 0 < b.re
c : ℂ
this✝ : b ≠ 0
h : (-↑π * b).re < 0
t : ℝ
this :
  ∀ (x : ℝ),
    ↑(-2 * π * x * t) * I + -↑π * b * ↑x ^ 2 + 2 * ↑π * c * ↑x =
      -↑π * b * ↑x ^ 2 + (-2 * ↑π * I * ↑t + 2 * ↑π * c) * ↑x + 0
⊢ -(↑π ^ 2 * I * ↑t * c * b * 8) + ↑π ^ 2 * I ^ 2 * ↑t ^ 2 * b * 4 + ↑π ^ 2 * c ^ 2 * b * 4 =
    -(↑π ^ 2 * I * ↑t * c * b * 8) + (-(↑π ^ 2 * I ^ 2 * c ^ 2 * b * 4) - ↑π ^ 2 * ↑t ^ 2 * b * 4)

Proof state:
case h.e_a.hx
b : ℂ
hb : 0 < b.re
c : ℂ
this✝ : b ≠ 0
h : (-↑π * b).re < 0
t : ℝ
this :
  ∀ (x : ℝ),
    ↑(-2 * π * x * t) * I + -↑π * b * ↑x ^ 2 + 2 * ↑π * c * ↑x =
      -↑π * b * ↑x ^ 2 + (-2 * ↑π * I * ↑t + 2 * ↑π * c) * ↑x + 0
⊢ 0 ≤ b.re ∨ ¬b.im = 0

Tactic:
exact Or.inl hb.le

Result:
no goals