awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ℝ ι
y : ι → ℝ
⊢ -(b * HPow.hPow (β := ℕ) (↑(Norm.norm (E := EuclideanSpace ℝ ι) (WithLp.toLp 2 y)) : ℂ) 2) =
    -b * ∑ i : ι, HPow.hPow (β := ℕ) (↑(y i) : ℂ) 2
have h : HPow.hPow (β := ℕ) (↑√(∑ x : ι, HPow.hPow (β := ℕ) (y x) 2) : ℂ) 2 = ∑ i : ι, HPow.hPow (β := ℕ) (↑(y i) : ℂ) 2 ∨ b = 0
Tactic: simp only [EuclideanSpace.norm_eq, norm_eq_abs, sq_abs, neg_mul, neg_inj, mul_eq_mul_left_iff]
-- 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 ℝ ι
y : ι → ℝ
⊢ HPow.hPow (β := ℕ) (↑√(∑ x : ι, HPow.hPow (β := ℕ) (y x) 2) : ℂ) 2 = ∑ i : ι, HPow.hPow (β := ℕ) (↑(y i) : ℂ) 2 ∨
    b = 0
have h : HPow.hPow (β := ℕ) (√(∑ x : ι, HPow.hPow (β := ℕ) (y x) 2)) 2 = ∑ i : ι, HPow.hPow (β := ℕ) (y i) 2 ∨ b = 0
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 ℝ ι
y : ι → ℝ
⊢ HPow.hPow (β := ℕ) (√(∑ x : ι, HPow.hPow (β := ℕ) (y x) 2)) 2 = ∑ i : ι, HPow.hPow (β := ℕ) (y i) 2 ∨ b = 0
have h : HPow.hPow (β := ℕ) (√(∑ x : ι, HPow.hPow (β := ℕ) (y x) 2)) 2 = ∑ i : ι, HPow.hPow (β := ℕ) (y i) 2
Tactic: left
-- 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 ℝ ι
y : ι → ℝ
⊢ HPow.hPow (β := ℕ) (√(∑ x : ι, HPow.hPow (β := ℕ) (y x) 2)) 2 = ∑ i : ι, HPow.hPow (β := ℕ) (y i) 2
have h : LE.le (α := ℝ) 0 (∑ x : ι, HPow.hPow (β := ℕ) (y x) 2)
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 ℝ ι
y : ι → ℝ
⊢ c * (↑⟪w, WithLp.toLp 2 y⟫ : ℂ) = ∑ i : ι, c * (↑(w.ofLp i) : ℂ) * (↑(y i) : ℂ)
have h : Eq (α := ℂ) (∑ i : ι, c * ((↑(y i) : ℂ) * (↑(w.ofLp i) : ℂ))) (∑ x : ι, c * ((↑(w.ofLp x) : ℂ) * (↑(y x) : ℂ)))
Tactic: simp only [PiLp.inner_apply, RCLike.inner_apply, conj_trivial, ofReal_sum, ofReal_mul,
      Finset.mul_sum, 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 ℝ ι
⊢ HPow.hPow (β := ℕ) c 2 * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 = ∑ i : ι, HPow.hPow (β := ℕ) (c * (↑(w.ofLp i) : ℂ)) 2
have h : HPow.hPow (β := ℕ) c 2 * HPow.hPow (β := ℕ) (↑√(∑ x : ι, HPow.hPow (β := ℕ) (w.ofLp x) 2) : ℂ) 2 =
  HPow.hPow (β := ℕ) c 2 * ∑ i : ι, HPow.hPow (β := ℕ) (↑(w.ofLp i) : ℂ) 2
Tactic: simp only [EuclideanSpace.norm_eq, Real.norm_eq_abs, sq_abs, mul_pow, ← 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 ℝ ι
⊢ HPow.hPow (β := ℕ) c 2 * HPow.hPow (β := ℕ) (↑√(∑ x : ι, HPow.hPow (β := ℕ) (w.ofLp x) 2) : ℂ) 2 =
    HPow.hPow (β := ℕ) c 2 * ∑ i : ι, HPow.hPow (β := ℕ) (↑(w.ofLp i) : ℂ) 2
have h : HPow.hPow (β := ℕ) (↑√(∑ x : ι, HPow.hPow (β := ℕ) (w.ofLp x) 2) : ℂ) 2 =
  ∑ i : ι, HPow.hPow (β := ℕ) (↑(w.ofLp i) : ℂ) 2
Tactic: congr
-- 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 ℝ ι
⊢ HPow.hPow (β := ℕ) (↑√(∑ x : ι, HPow.hPow (β := ℕ) (w.ofLp x) 2) : ℂ) 2 =
    ∑ i : ι, HPow.hPow (β := ℕ) (↑(w.ofLp i) : ℂ) 2
have h : HPow.hPow (β := ℕ) (√(∑ x : ι, HPow.hPow (β := ℕ) (w.ofLp x) 2)) 2 = ∑ i : ι, HPow.hPow (β := ℕ) (w.ofLp i) 2
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 ℝ ι
⊢ HPow.hPow (β := ℕ) (√(∑ x : ι, HPow.hPow (β := ℕ) (w.ofLp x) 2)) 2 = ∑ i : ι, HPow.hPow (β := ℕ) (w.ofLp i) 2
have h : LE.le (α := ℝ) 0 (∑ x : ι, HPow.hPow (β := ℕ) (w.ofLp 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))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      cexp (-b * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2 + c * (↑⟪w, v⟫ : ℂ))) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Module.finrank ℝ V) : ℂ) 2 *
      cexp (HPow.hPow (β := ℕ) c 2 * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 / (4 * b))
have rw : (@integral _ _ _ _
    (WithLp.measurableSpace 2 ((i : Fin (Module.finrank ℝ V)) → (fun (x : Fin (Module.finrank ℝ V)) ↦ ℝ) i)) volume
    fun (x : EuclideanSpace ℝ (Fin (Module.finrank ℝ V))) ↦
    cexp
      (-b *
          HPow.hPow (β := ℕ)
            (↑(Norm.norm (E := V) ((e : (a : EuclideanSpace ℝ (Fin (Module.finrank ℝ V))) → V) x : V)) : ℂ) 2 +
        c * (↑⟪w, (e : (a : EuclideanSpace ℝ (Fin (Module.finrank ℝ V))) → V) x⟫ : ℂ))) =
  ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Module.finrank ℝ V) : ℂ) 2 *
    cexp (HPow.hPow (β := ℕ) c 2 * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 / (4 * b))
Tactic: rw [← e.measurePreserving.integral_comp 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))
⊢ (@integral _ _ _ _
      (WithLp.measurableSpace 2 ((i : Fin (Module.finrank ℝ V)) → (fun (x : Fin (Module.finrank ℝ V)) ↦ ℝ) i)) volume
      fun (x : EuclideanSpace ℝ (Fin (Module.finrank ℝ V))) ↦
      cexp
        (-b *
            HPow.hPow (β := ℕ)
              (↑(Norm.norm (E := V) ((e : (a : EuclideanSpace ℝ (Fin (Module.finrank ℝ V))) → V) x : V)) : ℂ) 2 +
          c * (↑⟪w, (e : (a : EuclideanSpace ℝ (Fin (Module.finrank ℝ V))) → V) x⟫ : ℂ))) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Module.finrank ℝ V) : ℂ) 2 *
      cexp (HPow.hPow (β := ℕ) c 2 * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 / (4 * b))
have h : ∀ (x : EuclideanSpace ℝ (Fin (Module.finrank ℝ V))),
  Norm.norm (E := V) ((e : (a : EuclideanSpace ℝ (Fin (Module.finrank ℝ V))) → V) x : V) = ‖x‖
Tactic: convert! integral_cexp_neg_mul_sq_norm_add_of_euclideanSpace hb c (e.symm w)
-- 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))
h :
  ∀ (x : EuclideanSpace ℝ (Fin (Module.finrank ℝ V))),
    Norm.norm (E := V) ((e : (a : EuclideanSpace ℝ (Fin (Module.finrank ℝ V))) → V) x : V) = ‖x‖
⊢ (@integral _ _ _ _
      (WithLp.measurableSpace 2 ((i : Fin (Module.finrank ℝ V)) → (fun (x : Fin (Module.finrank ℝ V)) ↦ ℝ) i)) volume
      fun (x : EuclideanSpace ℝ (Fin (Module.finrank ℝ V))) ↦
      cexp
        (-b *
            HPow.hPow (β := ℕ)
              (↑(Norm.norm (E := V) ((e : (a : EuclideanSpace ℝ (Fin (Module.finrank ℝ V))) → V) x : V)) : ℂ) 2 +
          c * (↑⟪w, (e : (a : EuclideanSpace ℝ (Fin (Module.finrank ℝ V))) → V) x⟫ : ℂ))) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Module.finrank ℝ V) : ℂ) 2 *
      cexp (HPow.hPow (β := ℕ) c 2 * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 / (4 * b))
have h₁ : ∀ (x : EuclideanSpace ℝ (Fin (Module.finrank ℝ V))),
  ⟪w, (e : (a : EuclideanSpace ℝ (Fin (Module.finrank ℝ V))) → V) x⟫ =
    ⟪(e.symm : (a : V) → EuclideanSpace ℝ (Fin (Module.finrank ℝ V))) w, x⟫
Tactic: convert! integral_cexp_neg_mul_sq_norm_add_of_euclideanSpace hb c (e.symm w)
-- 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))
h :
  ∀ (x : EuclideanSpace ℝ (Fin (Module.finrank ℝ V))),
    Norm.norm (E := V) ((e : (a : EuclideanSpace ℝ (Fin (Module.finrank ℝ V))) → V) x : V) = ‖x‖
h₁ :
  ∀ (x : EuclideanSpace ℝ (Fin (Module.finrank ℝ V))),
    ⟪w, (e : (a : EuclideanSpace ℝ (Fin (Module.finrank ℝ V))) → V) x⟫ =
      ⟪(e.symm : (a : V) → EuclideanSpace ℝ (Fin (Module.finrank ℝ V))) w, x⟫
⊢ (@integral _ _ _ _
      (WithLp.measurableSpace 2 ((i : Fin (Module.finrank ℝ V)) → (fun (x : Fin (Module.finrank ℝ V)) ↦ ℝ) i)) volume
      fun (x : EuclideanSpace ℝ (Fin (Module.finrank ℝ V))) ↦
      cexp
        (-b *
            HPow.hPow (β := ℕ)
              (↑(Norm.norm (E := V) ((e : (a : EuclideanSpace ℝ (Fin (Module.finrank ℝ V))) → V) x : V)) : ℂ) 2 +
          c * (↑⟪w, (e : (a : EuclideanSpace ℝ (Fin (Module.finrank ℝ V))) → V) x⟫ : ℂ))) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Module.finrank ℝ V) : ℂ) 2 *
      cexp (HPow.hPow (β := ℕ) c 2 * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 / (4 * b))
have h₂ : Module.finrank ℝ V = Fintype.card (Fin (Module.finrank ℝ V))
Tactic: convert! integral_cexp_neg_mul_sq_norm_add_of_euclideanSpace hb c (e.symm w)
-- 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))
h :
  ∀ (x : EuclideanSpace ℝ (Fin (Module.finrank ℝ V))),
    Norm.norm (E := V) ((e : (a : EuclideanSpace ℝ (Fin (Module.finrank ℝ V))) → V) x : V) = ‖x‖
h₁ :
  ∀ (x : EuclideanSpace ℝ (Fin (Module.finrank ℝ V))),
    ⟪w, (e : (a : EuclideanSpace ℝ (Fin (Module.finrank ℝ V))) → V) x⟫ =
      ⟪(e.symm : (a : V) → EuclideanSpace ℝ (Fin (Module.finrank ℝ V))) w, x⟫
h₂ : Module.finrank ℝ V = Fintype.card (Fin (Module.finrank ℝ V))
⊢ (@integral _ _ _ _
      (WithLp.measurableSpace 2 ((i : Fin (Module.finrank ℝ V)) → (fun (x : Fin (Module.finrank ℝ V)) ↦ ℝ) i)) volume
      fun (x : EuclideanSpace ℝ (Fin (Module.finrank ℝ V))) ↦
      cexp
        (-b *
            HPow.hPow (β := ℕ)
              (↑(Norm.norm (E := V) ((e : (a : EuclideanSpace ℝ (Fin (Module.finrank ℝ V))) → V) x : V)) : ℂ) 2 +
          c * (↑⟪w, (e : (a : EuclideanSpace ℝ (Fin (Module.finrank ℝ V))) → V) x⟫ : ℂ))) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Module.finrank ℝ V) : ℂ) 2 *
      cexp (HPow.hPow (β := ℕ) c 2 * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 / (4 * b))
have h₃ : ‖w‖ =
  Norm.norm (E := EuclideanSpace ℝ (Fin (Module.finrank ℝ V)))
    ((e.symm : (a : V) → EuclideanSpace ℝ (Fin (Module.finrank ℝ V))) w : EuclideanSpace ℝ (Fin (Module.finrank ℝ V)))
Tactic: convert! integral_cexp_neg_mul_sq_norm_add_of_euclideanSpace hb c (e.symm w)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : FiniteDimensional ℝ V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
b : ℝ
hb : 0 < b
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦ rexp (-b * HPow.hPow (β := ℕ) ‖v‖ 2)) =
    (π / b) ^ HDiv.hDiv (α := ℝ) (↑(Module.finrank ℝ V) : ℝ) 2
have rw : (↑(@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦ rexp (-b * HPow.hPow (β := ℕ) ‖v‖ 2)) : ℂ) =
  (↑((π / b) ^ HDiv.hDiv (α := ℝ) (↑(Module.finrank ℝ V) : ℝ) 2) : ℂ)
Tactic: rw [← ofReal_inj]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : FiniteDimensional ℝ V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
b : ℝ
hb : 0 < b
⊢ (↑(@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦ rexp (-b * HPow.hPow (β := ℕ) ‖v‖ 2)) : ℂ) =
    (↑((π / b) ^ HDiv.hDiv (α := ℝ) (↑(Module.finrank ℝ V) : ℝ) 2) : ℂ)
have h : (↑(@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦ rexp (-b * HPow.hPow (β := ℕ) ‖v‖ 2)) : ℂ) =
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
    cexp (-(↑b : ℂ) * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2)
Tactic: convert! integral_cexp_neg_mul_sq_norm (show 0 < (b : ℂ).re from hb) (V := V)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : FiniteDimensional ℝ V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
b : ℝ
hb : 0 < b
h :
  (↑(@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦ rexp (-b * HPow.hPow (β := ℕ) ‖v‖ 2)) : ℂ) =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      cexp (-(↑b : ℂ) * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2)
⊢ (↑(@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦ rexp (-b * HPow.hPow (β := ℕ) ‖v‖ 2)) : ℂ) =
    (↑((π / b) ^ HDiv.hDiv (α := ℝ) (↑(Module.finrank ℝ V) : ℝ) 2) : ℂ)
have h₁ : (↑((π / b) ^ HDiv.hDiv (α := ℝ) (↑(Module.finrank ℝ V) : ℝ) 2) : ℂ) =
  ((↑π : ℂ) / (↑b : ℂ)) ^ HDiv.hDiv (α := ℂ) (↑(Module.finrank ℝ V) : ℂ) 2
Tactic: convert! integral_cexp_neg_mul_sq_norm (show 0 < (b : ℂ).re from hb) (V := V)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : FiniteDimensional ℝ V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
b : ℝ
hb : 0 < b
⊢ Eq (α := ℂ)
    ((ofRealLI : (a : ℝ) → ℂ)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦ rexp (-b * HPow.hPow (β := ℕ) ‖v‖ 2)) :
      ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        cexp (-(↑b : ℂ) * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2) :
      ℂ)
have h : Eq (α := ℂ)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
    (ofRealLI : (a : ℝ) → ℂ) (rexp (-b * HPow.hPow (β := ℕ) ‖x‖ 2)))
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
    cexp (-(↑b : ℂ) * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2))
Tactic: rw [← ofRealLI.integral_comp_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : FiniteDimensional ℝ V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
b : ℝ
hb : 0 < b
⊢ (↑((π / b) ^ HDiv.hDiv (α := ℝ) (↑(Module.finrank ℝ V) : ℝ) 2) : ℂ) =
    ((↑π : ℂ) / (↑b : ℂ)) ^ HDiv.hDiv (α := ℂ) (↑(Module.finrank ℝ V) : ℂ) 2
have h : (↑(π / b) : ℂ) ^ (↑(HDiv.hDiv (α := ℝ) (↑(Module.finrank ℝ V) : ℝ) 2) : ℂ) =
  (↑(π / b) : ℂ) ^ HDiv.hDiv (α := ℂ) (↑(Module.finrank ℝ V) : ℂ) 2
Tactic: rw [← ofReal_div, ofReal_cpow (by positivity)]
-- 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
x w : V
⊢ 𝓕 (E := (v : V) → ℂ) (fun (v : V) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪x, v⟫ : ℂ)))
      w =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Module.finrank ℝ V) : ℂ) 2 *
      cexp (-HPow.hPow (β := ℕ) (↑π : ℂ) 2 * HPow.hPow (β := ℕ) (↑‖x - w‖ : ℂ) 2 / b)
have simp : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
    cexp
      (-(2 * (↑π : ℂ) * (↑⟪w, v⟫ : ℂ) * I) +
        (-(b * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2) + 2 * (↑π : ℂ) * I * (↑⟪x, v⟫ : ℂ)))) =
  ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Module.finrank ℝ V) : ℂ) 2 *
    cexp (-(HPow.hPow (β := ℕ) (↑π : ℂ) 2 * HPow.hPow (β := ℕ) (↑‖x - w‖ : ℂ) 2) / b)
Tactic: simp only [neg_mul, fourier_eq', ofReal_neg, ofReal_mul, ofReal_ofNat,
    smul_eq_mul, ← Complex.exp_add, real_inner_comm w]
-- 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
x w : V
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      cexp
        (-(2 * (↑π : ℂ) * (↑⟪w, v⟫ : ℂ) * I) +
          (-(b * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2) + 2 * (↑π : ℂ) * I * (↑⟪x, v⟫ : ℂ)))) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Module.finrank ℝ V) : ℂ) 2 *
      cexp (-(HPow.hPow (β := ℕ) (↑π : ℂ) 2 * HPow.hPow (β := ℕ) (↑‖x - w‖ : ℂ) 2) / b)
have h : ∀ (v : V),
  cexp
      (-(2 * (↑π : ℂ) * (↑⟪w, v⟫ : ℂ) * I) +
        (-(b * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2) + 2 * (↑π : ℂ) * I * (↑⟪x, v⟫ : ℂ))) =
    cexp (-b * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪x - w, v⟫ : ℂ))
Tactic: convert! integral_cexp_neg_mul_sq_norm_add hb (2 * π * Complex.I) (x - w) using 3 with v
-- 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
x w : V
h :
  ∀ (v : V),
    cexp
        (-(2 * (↑π : ℂ) * (↑⟪w, v⟫ : ℂ) * I) +
          (-(b * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2) + 2 * (↑π : ℂ) * I * (↑⟪x, v⟫ : ℂ))) =
      cexp (-b * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪x - w, v⟫ : ℂ))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      cexp
        (-(2 * (↑π : ℂ) * (↑⟪w, v⟫ : ℂ) * I) +
          (-(b * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2) + 2 * (↑π : ℂ) * I * (↑⟪x, v⟫ : ℂ)))) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Module.finrank ℝ V) : ℂ) 2 *
      cexp (-(HPow.hPow (β := ℕ) (↑π : ℂ) 2 * HPow.hPow (β := ℕ) (↑‖x - w‖ : ℂ) 2) / b)
have h₁ : -(HPow.hPow (β := ℕ) (↑π : ℂ) 2 * HPow.hPow (β := ℕ) (↑‖x - w‖ : ℂ) 2) / b =
  HPow.hPow (β := ℕ) (2 * (↑π : ℂ) * I) 2 * HPow.hPow (β := ℕ) (↑‖x - w‖ : ℂ) 2 / (4 * b)
Tactic: convert! integral_cexp_neg_mul_sq_norm_add hb (2 * π * Complex.I) (x - w) using 3 with v
-- 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
x w v : V
⊢ cexp
      (-(2 * (↑π : ℂ) * (↑⟪w, v⟫ : ℂ) * I) +
        (-(b * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2) + 2 * (↑π : ℂ) * I * (↑⟪x, v⟫ : ℂ))) =
    cexp (-b * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪x - w, v⟫ : ℂ))
have h : -(2 * (↑π : ℂ) * (↑⟪w, v⟫ : ℂ) * I) + (-(b * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2) + 2 * (↑π : ℂ) * I * (↑⟪x, v⟫ : ℂ)) =
  -b * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪x - w, v⟫ : ℂ)
Tactic: congr 1
-- 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
x w v : V
⊢ -(2 * (↑π : ℂ) * (↑⟪w, v⟫ : ℂ) * I) + (-(b * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2) + 2 * (↑π : ℂ) * I * (↑⟪x, v⟫ : ℂ)) =
    -b * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪x - w, v⟫ : ℂ)
have h : -(2 * (↑π : ℂ) * (↑⟪w, v⟫ : ℂ) * I) + (-(b * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2) + 2 * (↑π : ℂ) * I * (↑⟪x, v⟫ : ℂ)) =
  -(b * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2) + 2 * (↑π : ℂ) * I * ((↑⟪x, v⟫ : ℂ) - (↑⟪w, v⟫ : ℂ))
Tactic: simp [inner_sub_left]
-- 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
x w : V
⊢ 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 : ℂ
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : FiniteDimensional ℝ V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
x w : V
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 : ℂ
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : FiniteDimensional ℝ V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
x w : V
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 : ℂ
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
x w : V
⊢ -(HPow.hPow (β := ℕ) (↑π : ℂ) 2 * HPow.hPow (β := ℕ) (↑‖x - w‖ : ℂ) 2) / b =
    HPow.hPow (β := ℕ) (2 * (↑π : ℂ) * I) 2 * HPow.hPow (β := ℕ) (↑‖x - w‖ : ℂ) 2 / (4 * b)
have this : b ≠ 0
Tactic: have : b ≠ 0 := by contrapose! hb; rw [hb, zero_re]
-- 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
x w : V
this : b ≠ 0
⊢ -(HPow.hPow (β := ℕ) (↑π : ℂ) 2 * HPow.hPow (β := ℕ) (↑‖x - w‖ : ℂ) 2) / b =
    HPow.hPow (β := ℕ) (2 * (↑π : ℂ) * I) 2 * HPow.hPow (β := ℕ) (↑‖x - w‖ : ℂ) 2 / (4 * b)
have h : -(HPow.hPow (β := ℕ) (↑π : ℂ) 2 * HPow.hPow (β := ℕ) (↑‖x - w‖ : ℂ) 2) / b =
  -(HPow.hPow (α := ℂ) (β := ℕ) 2 2 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 * HPow.hPow (β := ℕ) (↑‖x - w‖ : ℂ) 2) / (4 * b)
Tactic: simp [mul_pow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
p b : ℝ
hb : 0 < b
hp : 1 < p
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ rexp (-b * x ^ p)) fun (x : ℝ) ↦ rexp (-x)
have rw : Tendsto (β := ℝ) (fun (x : ℝ) ↦ -x - -b * x ^ p) atTop atTop
Tactic: rw [isLittleO_exp_comp_exp_comp]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
p b : ℝ
hb : 0 < b
hp : 1 < p
this : Tendsto (β := ℝ) (fun (x : ℝ) ↦ x * (b * x ^ (p - 1) + -1)) atTop atTop
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ -x - -b * x ^ p) atTop atTop
have refine : EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ x * (b * x ^ (p - 1) + -1)) fun (x : ℝ) ↦ -x - -b * x ^ p
Tactic: refine Tendsto.congr' ?_ this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
p b : ℝ
hb : 0 < b
hp : 1 < p
this : Tendsto (β := ℝ) (fun (x : ℝ) ↦ x * (b * x ^ (p - 1) + -1)) atTop atTop
⊢ EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ x * (b * x ^ (p - 1) + -1)) fun (x : ℝ) ↦ -x - -b * x ^ p
have refine : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x), x * (b * x ^ (p - 1) + -1) = -x - -b * x ^ p
Tactic: refine eventuallyEq_of_mem (Ioi_mem_atTop (0 : ℝ)) (fun x hx => ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (hypothesis)
Goal:
p b : ℝ
hb : 0 < b
hp : 1 < p
this : Tendsto (β := ℝ) (fun (x : ℝ) ↦ x * (b * x ^ (p - 1) + -1)) atTop atTop
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ x * (b * x ^ (p - 1) + -1) = -x - -b * x ^ p
have hx₁ : 0 < x
Tactic: rw [mem_Ioi] at hx
Cleared hypotheses: hx