awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : 0 < b.re
t : ℂ
rw :
  ((↑π : ℂ) / - -b) ^ (1 / 2) * cexp (0 - HPow.hPow (β := ℕ) (I * t) 2 / (4 * -b)) =
    ((↑π : ℂ) / b) ^ (1 / 2) * cexp (-HPow.hPow (β := ℕ) t 2 / (4 * b))
rw₁ :
  ((↑π : ℂ) / b) ^ (1 / 2) * cexp (0 - HPow.hPow (β := ℕ) (I * t) 2 / (4 * -b)) =
    ((↑π : ℂ) / b) ^ (1 / 2) * cexp (-HPow.hPow (β := ℕ) t 2 / (4 * b))
rw₂ :
  ((↑π : ℂ) / b) ^ (1 / 2) * cexp (-(HPow.hPow (β := ℕ) (I * t) 2 / (4 * -b))) =
    ((↑π : ℂ) / b) ^ (1 / 2) * cexp (-HPow.hPow (β := ℕ) t 2 / (4 * b))
rw₃ :
  ((↑π : ℂ) / b) ^ (1 / 2) * cexp (-(HPow.hPow (β := ℕ) (I * t) 2 / -(4 * b))) =
    ((↑π : ℂ) / b) ^ (1 / 2) * cexp (-HPow.hPow (β := ℕ) t 2 / (4 * b))
rw₄ :
  ((↑π : ℂ) / b) ^ (1 / 2) * cexp (- -(HPow.hPow (β := ℕ) (I * t) 2 / (4 * b))) =
    ((↑π : ℂ) / b) ^ (1 / 2) * cexp (-HPow.hPow (β := ℕ) t 2 / (4 * b))
rw₅ :
  ((↑π : ℂ) / b) ^ (1 / 2) * cexp (HPow.hPow (β := ℕ) (I * t) 2 / (4 * b)) =
    ((↑π : ℂ) / b) ^ (1 / 2) * cexp (-HPow.hPow (β := ℕ) t 2 / (4 * b))
rw₆ :
  ((↑π : ℂ) / b) ^ (1 / 2) * cexp (HPow.hPow (β := ℕ) I 2 * HPow.hPow (β := ℕ) t 2 / (4 * b)) =
    ((↑π : ℂ) / b) ^ (1 / 2) * cexp (-HPow.hPow (β := ℕ) t 2 / (4 * b))
rw₇ :
  ((↑π : ℂ) / b) ^ (1 / 2) * cexp (-1 * HPow.hPow (β := ℕ) t 2 / (4 * b)) =
    ((↑π : ℂ) / b) ^ (1 / 2) * cexp (-HPow.hPow (β := ℕ) t 2 / (4 * b))
rw₈ :
  ((↑π : ℂ) / b) ^ (1 / 2) * cexp (-HPow.hPow (β := ℕ) t 2 / (4 * b)) =
    ((↑π : ℂ) / b) ^ (1 / 2) * cexp (-HPow.hPow (β := ℕ) t 2 / (4 * b))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
      cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + I * t * (↑x : ℂ) + 0)) =
    ((↑π : ℂ) / b) ^ (1 / 2) * cexp (-HPow.hPow (β := ℕ) t 2 / (4 * b))
have rw₉ : cexp (-HPow.hPow (β := ℕ) t 2 / (4 * b)) * ((↑π : ℂ) / b) ^ (1 / 2) =
  cexp (-HPow.hPow (β := ℕ) t 2 / (4 * b)) * ((↑π : ℂ) / b) ^ (1 / 2)
Tactic: rw [integral_cexp_quadratic (show (-b).re < 0 by rwa [neg_re, neg_lt_zero]), neg_neg, zero_sub,
    mul_neg, div_neg, neg_neg, mul_pow, I_sq, neg_one_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : 0 < b.re
c : ℂ
⊢ b ≠ 0
have contrapose! : ∀ (hb : b = 0), b.re ≤ 0
Tactic: contrapose! hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b c : ℂ
hb : b = 0
⊢ b.re ≤ 0
have rw : re 0 ≤ 0
Tactic: rw [hb, zero_re]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b c : ℂ
hb : b = 0
rw : re 0 ≤ 0
⊢ b.re ≤ 0
have rw₁ : LE.le (α := ℝ) 0 0
Tactic: rw [hb, zero_re]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (hypothesis)
Goal:
b : ℂ
hb : 0 < b.re
c : ℂ
⊢ (𝓕 (E := (x : ℝ) → ℂ) fun (x : ℝ) ↦
      cexp (-(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + 2 * (↑π : ℂ) * c * (↑x : ℂ))) =
    fun (t : ℝ) ↦ 1 / b ^ (1 / 2) * cexp (-(↑π : ℂ) / b * HPow.hPow (β := ℕ) ((↑t : ℂ) + I * c) 2)
have this : b ≠ 0
Tactic: haveI : b ≠ 0 := by contrapose! hb; rw [hb, zero_re]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (hypothesis)
Goal:
b : ℂ
hb : 0 < b.re
c : ℂ
this : b ≠ 0
⊢ (𝓕 (E := (x : ℝ) → ℂ) fun (x : ℝ) ↦
      cexp (-(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + 2 * (↑π : ℂ) * c * (↑x : ℂ))) =
    fun (t : ℝ) ↦ 1 / b ^ (1 / 2) * cexp (-(↑π : ℂ) / b * HPow.hPow (β := ℕ) ((↑t : ℂ) + I * c) 2)
have h : (-(↑π : ℂ) * b).re < 0
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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : 0 < b.re
c : ℂ
this : b ≠ 0
h : (-(↑π : ℂ) * b).re < 0
⊢ (𝓕 (E := (x : ℝ) → ℂ) fun (x : ℝ) ↦
      cexp (-(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + 2 * (↑π : ℂ) * c * (↑x : ℂ))) =
    fun (t : ℝ) ↦ 1 / b ^ (1 / 2) * cexp (-(↑π : ℂ) / b * HPow.hPow (β := ℕ) ((↑t : ℂ) + I * c) 2)
have h₁ : ∀ (t : ℝ),
  𝓕 (E := (x : ℝ) → ℂ)
      (fun (x : ℝ) ↦ cexp (-(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + 2 * (↑π : ℂ) * c * (↑x : ℂ))) t =
    1 / b ^ (1 / 2) * cexp (-(↑π : ℂ) / b * HPow.hPow (β := ℕ) ((↑t : ℂ) + I * c) 2)
Tactic: ext1 t
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : 0 < b.re
c : ℂ
this : b ≠ 0
h : (-(↑π : ℂ) * b).re < 0
t : ℝ
⊢ 𝓕 (E := (x : ℝ) → ℂ)
      (fun (x : ℝ) ↦ cexp (-(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + 2 * (↑π : ℂ) * c * (↑x : ℂ))) t =
    1 / b ^ (1 / 2) * cexp (-(↑π : ℂ) / b * HPow.hPow (β := ℕ) ((↑t : ℂ) + I * c) 2)
have h₁ : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ℝ) ↦
    cexp ((↑(-2 * π * v * t) : ℂ) * I + -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑v : ℂ) 2 + 2 * (↑π : ℂ) * c * (↑v : ℂ))) =
  1 / b ^ (1 / 2) * cexp (-(↑π : ℂ) / b * HPow.hPow (β := ℕ) ((↑t : ℂ) + I * c) 2)
Tactic: simp_rw [fourier_real_eq_integral_exp_smul, smul_eq_mul, ← Complex.exp_add, ← add_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : 0 < b.re
c : ℂ
this : b ≠ 0
h : (-(↑π : ℂ) * b).re < 0
t x : ℝ
⊢ (↑(-2 * π * x * t) : ℂ) * I + -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + 2 * (↑π : ℂ) * c * (↑x : ℂ) =
    -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + (-2 * (↑π : ℂ) * I * (↑t : ℂ) + 2 * (↑π : ℂ) * c) * (↑x : ℂ) + 0
have push_cast : -2 * (↑π : ℂ) * (↑x : ℂ) * (↑t : ℂ) * I + -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + 2 * (↑π : ℂ) * c * (↑x : ℂ) =
  -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + (-2 * (↑π : ℂ) * I * (↑t : ℂ) + 2 * (↑π : ℂ) * c) * (↑x : ℂ) + 0
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (hypothesis)
Goal:
b : ℂ
hb : 0 < b.re
c : ℂ
this : b ≠ 0
h : (-(↑π : ℂ) * b).re < 0
t : ℝ
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ℝ) ↦
      cexp
        ((↑(-2 * π * v * t) : ℂ) * I + -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑v : ℂ) 2 + 2 * (↑π : ℂ) * c * (↑v : ℂ))) =
    1 / b ^ (1 / 2) * cexp (-(↑π : ℂ) / b * HPow.hPow (β := ℕ) ((↑t : ℂ) + I * c) 2)
have this₁ : ∀ (x : ℝ),
  (↑(-2 * π * x * t) : ℂ) * I + -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + 2 * (↑π : ℂ) * c * (↑x : ℂ) =
    -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + (-2 * (↑π : ℂ) * I * (↑t : ℂ) + 2 * (↑π : ℂ) * c) * (↑x : ℂ) + 0
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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : 0 < b.re
c : ℂ
this_1 : b ≠ 0
h : (-(↑π : ℂ) * b).re < 0
t : ℝ
this :
  ∀ (x : ℝ),
    (↑(-2 * π * x * t) : ℂ) * I + -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + 2 * (↑π : ℂ) * c * (↑x : ℂ) =
      -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + (-2 * (↑π : ℂ) * I * (↑t : ℂ) + 2 * (↑π : ℂ) * c) * (↑x : ℂ) + 0
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ℝ) ↦
      cexp
        ((↑(-2 * π * v * t) : ℂ) * I + -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑v : ℂ) 2 + 2 * (↑π : ℂ) * c * (↑v : ℂ))) =
    1 / b ^ (1 / 2) * cexp (-(↑π : ℂ) / b * HPow.hPow (β := ℕ) ((↑t : ℂ) + I * c) 2)
have h₁ : ((↑π : ℂ) / ((↑π : ℂ) * b)) ^ (1 / 2) *
    cexp (0 - HPow.hPow (β := ℕ) (-(2 * (↑π : ℂ) * I * (↑t : ℂ)) + 2 * (↑π : ℂ) * c) 2 / (4 * -((↑π : ℂ) * b))) =
  1 / b ^ (1 / 2) * cexp (-(↑π : ℂ) / b * HPow.hPow (β := ℕ) ((↑t : ℂ) + I * c) 2)
Tactic: simp_rw [this, integral_cexp_quadratic h, neg_mul, neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : 0 < b.re
c : ℂ
this_1 : b ≠ 0
h : (-(↑π : ℂ) * b).re < 0
t : ℝ
this :
  ∀ (x : ℝ),
    (↑(-2 * π * x * t) : ℂ) * I + -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + 2 * (↑π : ℂ) * c * (↑x : ℂ) =
      -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + (-2 * (↑π : ℂ) * I * (↑t : ℂ) + 2 * (↑π : ℂ) * c) * (↑x : ℂ) + 0
⊢ ((↑π : ℂ) / ((↑π : ℂ) * b)) ^ (1 / 2) *
      cexp (0 - HPow.hPow (β := ℕ) (-(2 * (↑π : ℂ) * I * (↑t : ℂ)) + 2 * (↑π : ℂ) * c) 2 / (4 * -((↑π : ℂ) * b))) =
    1 / b ^ (1 / 2) * cexp (-(↑π : ℂ) / b * HPow.hPow (β := ℕ) ((↑t : ℂ) + I * c) 2)
have h₁ : ((↑π : ℂ) / ((↑π : ℂ) * b)) ^ (1 / 2) = 1 / b ^ (1 / 2)
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : 0 < b.re
c : ℂ
this_1 : b ≠ 0
h : (-(↑π : ℂ) * b).re < 0
t : ℝ
this :
  ∀ (x : ℝ),
    (↑(-2 * π * x * t) : ℂ) * I + -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + 2 * (↑π : ℂ) * c * (↑x : ℂ) =
      -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + (-2 * (↑π : ℂ) * I * (↑t : ℂ) + 2 * (↑π : ℂ) * c) * (↑x : ℂ) + 0
h₁ : ((↑π : ℂ) / ((↑π : ℂ) * b)) ^ (1 / 2) = 1 / b ^ (1 / 2)
⊢ ((↑π : ℂ) / ((↑π : ℂ) * b)) ^ (1 / 2) *
      cexp (0 - HPow.hPow (β := ℕ) (-(2 * (↑π : ℂ) * I * (↑t : ℂ)) + 2 * (↑π : ℂ) * c) 2 / (4 * -((↑π : ℂ) * b))) =
    1 / b ^ (1 / 2) * cexp (-(↑π : ℂ) / b * HPow.hPow (β := ℕ) ((↑t : ℂ) + I * c) 2)
have h₂ : 0 - HPow.hPow (β := ℕ) (-(2 * (↑π : ℂ) * I * (↑t : ℂ)) + 2 * (↑π : ℂ) * c) 2 / (4 * -((↑π : ℂ) * b)) =
  -(↑π : ℂ) / b * HPow.hPow (β := ℕ) ((↑t : ℂ) + I * c) 2
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : 0 < b.re
c : ℂ
this_1 : b ≠ 0
h : (-(↑π : ℂ) * b).re < 0
t : ℝ
this :
  ∀ (x : ℝ),
    (↑(-2 * π * x * t) : ℂ) * I + -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + 2 * (↑π : ℂ) * c * (↑x : ℂ) =
      -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + (-2 * (↑π : ℂ) * I * (↑t : ℂ) + 2 * (↑π : ℂ) * c) * (↑x : ℂ) + 0
⊢ ((↑π : ℂ) / ((↑π : ℂ) * b)) ^ (1 / 2) = 1 / b ^ (1 / 2)
have h₁ : b.arg ≠ π
Tactic: rw [← div_div, div_self <| ofReal_ne_zero.mpr pi_ne_zero, one_div, inv_cpow, ← one_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : 0 < b.re
c : ℂ
this_1 : b ≠ 0
h : (-(↑π : ℂ) * b).re < 0
t : ℝ
this :
  ∀ (x : ℝ),
    (↑(-2 * π * x * t) : ℂ) * I + -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + 2 * (↑π : ℂ) * c * (↑x : ℂ) =
      -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + (-2 * (↑π : ℂ) * I * (↑t : ℂ) + 2 * (↑π : ℂ) * c) * (↑x : ℂ) + 0
⊢ b.arg ≠ π
have h₁ : 0 ≤ b.re ∨ ¬b.im = 0
Tactic: rw [Ne, arg_eq_pi_iff, not_and_or, not_lt]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : 0 < b.re
c : ℂ
this_1 : b ≠ 0
h : (-(↑π : ℂ) * b).re < 0
t : ℝ
this :
  ∀ (x : ℝ),
    (↑(-2 * π * x * t) : ℂ) * I + -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + 2 * (↑π : ℂ) * c * (↑x : ℂ) =
      -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + (-2 * (↑π : ℂ) * I * (↑t : ℂ) + 2 * (↑π : ℂ) * c) * (↑x : ℂ) + 0
⊢ 0 - HPow.hPow (β := ℕ) (-(2 * (↑π : ℂ) * I * (↑t : ℂ)) + 2 * (↑π : ℂ) * c) 2 / (4 * -((↑π : ℂ) * b)) =
    -(↑π : ℂ) / b * HPow.hPow (β := ℕ) ((↑t : ℂ) + I * c) 2
have h₁ : HMul.hMul (α := ℂ) 0 4 * b -
    -(HPow.hPow (α := ℂ) (β := ℕ) 2 2 * (↑π : ℂ) * HPow.hPow (β := ℕ) (-(I * (↑t : ℂ)) + c) 2) =
  -((↑π : ℂ) * 4 * HPow.hPow (β := ℕ) ((↑t : ℂ) + I * c) 2)
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : 0 < b.re
c : ℂ
this_1 : b ≠ 0
h : (-(↑π : ℂ) * b).re < 0
t : ℝ
this :
  ∀ (x : ℝ),
    (↑(-2 * π * x * t) : ℂ) * I + -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + 2 * (↑π : ℂ) * c * (↑x : ℂ) =
      -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + (-2 * (↑π : ℂ) * I * (↑t : ℂ) + 2 * (↑π : ℂ) * c) * (↑x : ℂ) + 0
⊢ HMul.hMul (α := ℂ) 0 4 * b -
      -(HPow.hPow (α := ℂ) (β := ℕ) 2 2 * (↑π : ℂ) * HPow.hPow (β := ℕ) (-(I * (↑t : ℂ)) + c) 2) =
    -((↑π : ℂ) * 4 * HPow.hPow (β := ℕ) ((↑t : ℂ) + I * c) 2)
have h₁ : -((↑π : ℂ) * I * (↑t : ℂ) * c * 8) + (↑π : ℂ) * HPow.hPow (β := ℕ) I 2 * HPow.hPow (β := ℕ) (↑t : ℂ) 2 * 4 +
    (↑π : ℂ) * HPow.hPow (β := ℕ) c 2 * 4 =
  -((↑π : ℂ) * I * (↑t : ℂ) * c * 8) - (↑π : ℂ) * HPow.hPow (β := ℕ) I 2 * HPow.hPow (β := ℕ) c 2 * 4 -
    (↑π : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 * 4
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : 0 < b.re
c : ℂ
this_1 : b ≠ 0
h : (-(↑π : ℂ) * b).re < 0
t : ℝ
this :
  ∀ (x : ℝ),
    (↑(-2 * π * x * t) : ℂ) * I + -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + 2 * (↑π : ℂ) * c * (↑x : ℂ) =
      -(↑π : ℂ) * b * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + (-2 * (↑π : ℂ) * I * (↑t : ℂ) + 2 * (↑π : ℂ) * c) * (↑x : ℂ) + 0
⊢ -((↑π : ℂ) * I * (↑t : ℂ) * c * 8) + (↑π : ℂ) * HPow.hPow (β := ℕ) I 2 * HPow.hPow (β := ℕ) (↑t : ℂ) 2 * 4 +
      (↑π : ℂ) * HPow.hPow (β := ℕ) c 2 * 4 =
    -((↑π : ℂ) * I * (↑t : ℂ) * c * 8) - (↑π : ℂ) * HPow.hPow (β := ℕ) I 2 * HPow.hPow (β := ℕ) c 2 * 4 -
      (↑π : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 * 4
have h₁ : -((↑π : ℂ) * I * (↑t : ℂ) * c * 8) + (↑π : ℂ) * -1 * HPow.hPow (β := ℕ) (↑t : ℂ) 2 * 4 +
    (↑π : ℂ) * HPow.hPow (β := ℕ) c 2 * 4 =
  -((↑π : ℂ) * I * (↑t : ℂ) * c * 8) - (↑π : ℂ) * -1 * HPow.hPow (β := ℕ) c 2 * 4 -
    (↑π : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 * 4
Tactic: simp only [I_sq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
ι : Type u_2
inst : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
⊢ @Integrable ℂ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (v : ι → ℝ) ↦
      cexp (HAdd.hAdd (α := ℂ) (-∑ i : ι, b i * HPow.hPow (β := ℕ) (↑(v i) : ℂ) 2) (∑ i : ι, c i * (↑(v i) : ℂ))))
    volume
have simp_rw : @Integrable ℂ _ _ _ MeasureSpace.toMeasurableSpace
  (fun (v : ι → ℝ) ↦ ∏ x : ι, cexp (-b x * HPow.hPow (β := ℕ) (↑(v x) : ℂ) 2 + c x * (↑(v x) : ℂ))) volume
Tactic: simp_rw [← Finset.sum_neg_distrib, ← Finset.sum_add_distrib, Complex.exp_sum, ← neg_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
ι : Type u_2
inst : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
⊢ @Integrable ℂ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (v : ι → ℝ) ↦ ∏ x : ι, cexp (-b x * HPow.hPow (β := ℕ) (↑(v x) : ℂ) 2 + c x * (↑(v x) : ℂ))) volume
have apply : ∀ (i : ι),
  @Integrable ℂ _ _ ℝ MeasureSpace.toMeasurableSpace
    ((fun (i : ι) (v : ℝ) ↦ cexp (-b i * HPow.hPow (β := ℕ) (↑v : ℂ) 2 + c i * (↑v : ℂ))) i) volume
Tactic: apply Integrable.fintype_prod (f := fun i (v : ℝ) ↦ cexp (-b i * v ^ 2 + c i * v)) (fun i ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
ι : Type u_2
inst : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
i : ι
⊢ @Integrable ℂ _ _ ℝ MeasureSpace.toMeasurableSpace
    ((fun (i : ι) (v : ℝ) ↦ cexp (-b i * HPow.hPow (β := ℕ) (↑v : ℂ) 2 + c i * (↑v : ℂ))) i) volume
have h : ∀ (x : ℝ),
  -b i * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + c i * (↑x : ℂ) = -b i * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + c i * (↑x : ℂ) + 0
Tactic: convert! integrable_cexp_quadratic (hb i) (c i) 0 using 3 with x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
ι : Type u_2
inst : Fintype ι
hb : 0 < b.re
c : ι → ℂ
⊢ @Integrable ℂ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (v : ι → ℝ) ↦ cexp (-b * ∑ i : ι, HPow.hPow (β := ℕ) (↑(v i) : ℂ) 2 + ∑ i : ι, c i * (↑(v i) : ℂ))) volume
have simp_rw : @Integrable ℂ _ _ _ MeasureSpace.toMeasurableSpace
  (fun (v : ι → ℝ) ↦
    cexp (HAdd.hAdd (α := ℂ) (-∑ i : ι, b * HPow.hPow (β := ℕ) (↑(v i) : ℂ) 2) (∑ i : ι, c i * (↑(v i) : ℂ))))
  volume
Tactic: simp_rw [neg_mul, Finset.mul_sum]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
ι : Type u_2
inst : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
⊢ @Integrable ℂ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (v : EuclideanSpace ℝ ι) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2 + c * (↑⟪w, v⟫ : ℂ))) volume
have rw : @Integrable.{0, u_2} ℂ _ _ (ι → ℝ) (MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ))
  ((fun (v : EuclideanSpace ℝ ι) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2 + c * (↑⟪w, v⟫ : ℂ))) ∘ WithLp.toLp 2)
  (volume : Measure (ι → ℝ))
Tactic: rw [← (PiLp.volume_preserving_toLp ι).integrable_comp_emb
    (MeasurableEquiv.toLp 2 _).measurableEmbedding]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
ι : Type u_2
inst : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
⊢ @Integrable.{0, u_2} ℂ _ _ (ι → ℝ) (MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ))
    ((fun (v : EuclideanSpace ℝ ι) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2 + c * (↑⟪w, v⟫ : ℂ))) ∘ WithLp.toLp 2)
    (volume : Measure (ι → ℝ))
have simp : @Integrable ℂ _ _ _ (MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ))
  (fun (x : ι → ℝ) ↦
    cexp
      (-(b * HPow.hPow (β := ℕ) (↑(Norm.norm (E := EuclideanSpace ℝ ι) (WithLp.toLp 2 x)) : ℂ) 2) +
        c * (↑⟪w, WithLp.toLp 2 x⟫ : ℂ)))
  (volume : Measure (ι → ℝ))
Tactic: simp only [neg_mul, Function.comp_def]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
ι : Type u_2
inst : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
⊢ @Integrable ℂ _ _ _ (MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ))
    (fun (x : ι → ℝ) ↦
      cexp
        (-(b * HPow.hPow (β := ℕ) (↑(Norm.norm (E := EuclideanSpace ℝ ι) (WithLp.toLp 2 x)) : ℂ) 2) +
          c * (↑⟪w, WithLp.toLp 2 x⟫ : ℂ)))
    (volume : Measure (ι → ℝ))
have h : ∀ (v : ι → ℝ),
  -(b * HPow.hPow (β := ℕ) (↑(Norm.norm (E := EuclideanSpace ℝ ι) (WithLp.toLp 2 v)) : ℂ) 2) +
      c * (↑⟪w, WithLp.toLp 2 v⟫ : ℂ) =
    -b * ∑ i : ι, HPow.hPow (β := ℕ) (↑(v i) : ℂ) 2 + ∑ i : ι, c * (↑(w.ofLp i) : ℂ) * (↑(v i) : ℂ)
Tactic: convert! integrable_cexp_neg_mul_sum_add hb (fun i ↦ c * w i) using 3 with v
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
ι : Type u_2
inst : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
v : ι → ℝ
⊢ -(b * HPow.hPow (β := ℕ) (↑(Norm.norm (E := EuclideanSpace ℝ ι) (WithLp.toLp 2 v)) : ℂ) 2) +
      c * (↑⟪w, WithLp.toLp 2 v⟫ : ℂ) =
    -b * ∑ i : ι, HPow.hPow (β := ℕ) (↑(v i) : ℂ) 2 + ∑ i : ι, c * (↑(w.ofLp i) : ℂ) * (↑(v i) : ℂ)
have h : -(b * HPow.hPow (β := ℕ) (↑√(∑ x : ι, HPow.hPow (β := ℕ) (v x) 2) : ℂ) 2) +
    ∑ i : ι, c * ((↑(v i) : ℂ) * (↑(w.ofLp i) : ℂ)) =
  HAdd.hAdd (α := ℂ) (-∑ x : ι, b * HPow.hPow (β := ℕ) (↑(v x) : ℂ) 2) (∑ x : ι, c * ((↑(w.ofLp x) : ℂ) * (↑(v x) : ℂ)))
Tactic: simp only [EuclideanSpace.norm_eq, norm_eq_abs, sq_abs, PiLp.inner_apply, RCLike.inner_apply,
    conj_trivial, ofReal_sum, ofReal_mul, Finset.mul_sum, neg_mul, Finset.sum_neg_distrib,
    mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
ι : Type u_2
inst : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
v : ι → ℝ
⊢ -(b * HPow.hPow (β := ℕ) (↑√(∑ x : ι, HPow.hPow (β := ℕ) (v x) 2) : ℂ) 2) +
      ∑ i : ι, c * ((↑(v i) : ℂ) * (↑(w.ofLp i) : ℂ)) =
    HAdd.hAdd (α := ℂ) (-∑ x : ι, b * HPow.hPow (β := ℕ) (↑(v x) : ℂ) 2)
      (∑ x : ι, c * ((↑(w.ofLp x) : ℂ) * (↑(v x) : ℂ)))
have h : -(b * (↑(HPow.hPow (β := ℕ) (√(∑ x : ι, HPow.hPow (β := ℕ) (v x) 2)) 2) : ℂ)) + ∑ x : ι, c * (↑(v x * w.ofLp x) : ℂ) =
  HAdd.hAdd (α := ℂ) (-∑ x : ι, b * (↑(HPow.hPow (β := ℕ) (v x) 2) : ℂ)) (∑ x : ι, c * (↑(w.ofLp x * v x) : ℂ))
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
ι : Type u_2
inst : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
v : ι → ℝ
⊢ -(b * (↑(HPow.hPow (β := ℕ) (√(∑ x : ι, HPow.hPow (β := ℕ) (v x) 2)) 2) : ℂ)) + ∑ x : ι, c * (↑(v x * w.ofLp x) : ℂ) =
    HAdd.hAdd (α := ℂ) (-∑ x : ι, b * (↑(HPow.hPow (β := ℕ) (v x) 2) : ℂ)) (∑ x : ι, c * (↑(w.ofLp x * v x) : ℂ))
have h : -(b * (↑(∑ x : ι, HPow.hPow (β := ℕ) (v x) 2) : ℂ)) + ∑ x : ι, c * (↑(v x * w.ofLp x) : ℂ) =
  HAdd.hAdd (α := ℂ) (-∑ x : ι, b * (↑(HPow.hPow (β := ℕ) (v x) 2) : ℂ)) (∑ x : ι, c * (↑(w.ofLp x * v x) : ℂ))
Tactic: rw [sq_sqrt]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
ι : Type u_2
inst : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
v : ι → ℝ
h :
  -(b * (↑(∑ x : ι, HPow.hPow (β := ℕ) (v x) 2) : ℂ)) + ∑ x : ι, c * (↑(v x * w.ofLp x) : ℂ) =
    HAdd.hAdd (α := ℂ) (-∑ x : ι, b * (↑(HPow.hPow (β := ℕ) (v x) 2) : ℂ)) (∑ x : ι, c * (↑(w.ofLp x * v x) : ℂ))
⊢ -(b * (↑(HPow.hPow (β := ℕ) (√(∑ x : ι, HPow.hPow (β := ℕ) (v x) 2)) 2) : ℂ)) + ∑ x : ι, c * (↑(v x * w.ofLp x) : ℂ) =
    HAdd.hAdd (α := ℂ) (-∑ x : ι, b * (↑(HPow.hPow (β := ℕ) (v x) 2) : ℂ)) (∑ x : ι, c * (↑(w.ofLp x * v x) : ℂ))
have h₁ : LE.le (α := ℝ) 0 (∑ x : ι, HPow.hPow (β := ℕ) (v x) 2)
Tactic: rw [sq_sqrt]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : FiniteDimensional ℝ V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
hb : 0 < b.re
c : ℂ
w : V
e : EuclideanSpace ℝ (Fin (Module.finrank ℝ V)) ≃ₗᵢ[ℝ] V :=
  LinearIsometryEquiv.symm (OrthonormalBasis.repr (stdOrthonormalBasis ℝ V))
⊢ @Integrable ℂ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (v : V) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2 + c * (↑⟪w, v⟫ : ℂ))) volume
have rw : @Integrable ℂ _ _ (EuclideanSpace ℝ (Fin (Module.finrank ℝ V)))
  (WithLp.measurableSpace 2 ((i : Fin (Module.finrank ℝ V)) → (fun (x : Fin (Module.finrank ℝ V)) ↦ ℝ) i))
  ((fun (v : V) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2 + c * (↑⟪w, v⟫ : ℂ))) ∘
    (⇑e : (a : EuclideanSpace ℝ (Fin (Module.finrank ℝ V))) → V))
  volume
Tactic: rw [← e.measurePreserving.integrable_comp_emb e.toHomeomorph.measurableEmbedding]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : FiniteDimensional ℝ V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
hb : 0 < b.re
c : ℂ
w : V
e : EuclideanSpace ℝ (Fin (Module.finrank ℝ V)) ≃ₗᵢ[ℝ] V :=
  LinearIsometryEquiv.symm (OrthonormalBasis.repr (stdOrthonormalBasis ℝ V))
⊢ @Integrable ℂ _ _ (EuclideanSpace ℝ (Fin (Module.finrank ℝ V)))
    (WithLp.measurableSpace 2 ((i : Fin (Module.finrank ℝ V)) → (fun (x : Fin (Module.finrank ℝ V)) ↦ ℝ) i))
    ((fun (v : V) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2 + c * (↑⟪w, v⟫ : ℂ))) ∘
      (⇑e : (a : EuclideanSpace ℝ (Fin (Module.finrank ℝ V))) → V))
    volume
have h : ∀ (v : EuclideanSpace ℝ (Fin (Module.finrank ℝ V))),
  ((fun (v : V) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2 + c * (↑⟪w, v⟫ : ℂ))) ∘
        (⇑e : (a : EuclideanSpace ℝ (Fin (Module.finrank ℝ V))) → V))
      v =
    cexp
      (-b * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2 +
        c * (↑⟪(e.symm : (a : V) → EuclideanSpace ℝ (Fin (Module.finrank ℝ V))) w, v⟫ : ℂ))
Tactic: convert! integrable_cexp_neg_mul_sq_norm_add_of_euclideanSpace hb c (e.symm w) with v
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
ι : Type u_2
inst : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
⊢ Eq (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ι → ℝ) ↦
      cexp (HAdd.hAdd (α := ℂ) (-∑ i : ι, b i * HPow.hPow (β := ℕ) (↑(v i) : ℂ) 2) (∑ i : ι, c i * (↑(v i) : ℂ))))
    (∏ i : ι, ((↑π : ℂ) / b i) ^ (1 / 2) * cexp (HPow.hPow (β := ℕ) (c i) 2 / (4 * b i)))
have simp_rw : Eq (α := ℂ)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ι → ℝ) ↦
    ∏ x : ι, cexp (-b x * HPow.hPow (β := ℕ) (↑(v x) : ℂ) 2 + c x * (↑(v x) : ℂ)))
  (∏ i : ι, ((↑π : ℂ) / b i) ^ (1 / 2) * cexp (HPow.hPow (β := ℕ) (c i) 2 / (4 * b i)))
Tactic: simp_rw [← Finset.sum_neg_distrib, ← Finset.sum_add_distrib, Complex.exp_sum, ← neg_mul]