awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
ι : Type u_2
inst : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
y : ι → ℝ
h : Eq (α := ℂ) (∑ i : ι, c * ((↑(y i) : ℂ) * (↑(w.ofLp i) : ℂ))) (∑ x : ι, c * ((↑(w.ofLp x) : ℂ) * (↑(y x) : ℂ)))
⊢ c * (↑⟪w, WithLp.toLp 2 y⟫ : ℂ) = ∑ i : ι, c * (↑(w.ofLp i) : ℂ) * (↑(y i) : ℂ)

Tactic:
simp only [PiLp.inner_apply, RCLike.inner_apply, conj_trivial, ofReal_sum, ofReal_mul,
      Finset.mul_sum, mul_assoc]

Premises used: Finset.mul_sum, mul_assoc, conj_trivial, Complex.ofReal_sum, RCLike.inner_apply, PiLp.inner_apply, Complex.ofReal_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
ι : Type u_2
inst : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
y : ι → ℝ
⊢ Eq (α := ℂ) (∑ i : ι, c * ((↑(y i) : ℂ) * (↑(w.ofLp i) : ℂ))) (∑ x : ι, c * ((↑(w.ofLp x) : ℂ) * (↑(y x) : ℂ)))

Tactic:
simp_rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
ι : Type u_2
inst : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
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
⊢ HPow.hPow (β := ℕ) c 2 * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 = ∑ i : ι, HPow.hPow (β := ℕ) (c * (↑(w.ofLp i) : ℂ)) 2

Tactic:
simp only [EuclideanSpace.norm_eq, Real.norm_eq_abs, sq_abs, mul_pow, ← Finset.mul_sum]

Premises used: Finset.mul_sum, EuclideanSpace.norm_eq, sq_abs, mul_pow, Real.norm_eq_abs
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
ι : Type u_2
inst : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
h :
  HPow.hPow (β := ℕ) (↑√(∑ x : ι, HPow.hPow (β := ℕ) (w.ofLp x) 2) : ℂ) 2 =
    ∑ i : ι, HPow.hPow (β := ℕ) (↑(w.ofLp i) : ℂ) 2
⊢ 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:
congr
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
ι : Type u_2
inst : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
h : HPow.hPow (β := ℕ) (√(∑ x : ι, HPow.hPow (β := ℕ) (w.ofLp x) 2)) 2 = ∑ i : ι, HPow.hPow (β := ℕ) (w.ofLp i) 2
⊢ HPow.hPow (β := ℕ) (↑√(∑ x : ι, HPow.hPow (β := ℕ) (w.ofLp x) 2) : ℂ) 2 =
    ∑ i : ι, HPow.hPow (β := ℕ) (↑(w.ofLp i) : ℂ) 2

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
ι : Type u_2
inst : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
h : LE.le (α := ℝ) 0 (∑ x : ι, HPow.hPow (β := ℕ) (w.ofLp x) 2)
⊢ HPow.hPow (β := ℕ) (√(∑ x : ι, HPow.hPow (β := ℕ) (w.ofLp x) 2)) 2 = ∑ i : ι, HPow.hPow (β := ℕ) (w.ofLp i) 2

Tactic:
rw [sq_sqrt]

Premises used: Real.sq_sqrt
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
ι : Type u_2
inst : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
i : ι
_hi : Membership.mem (γ := Finset ι) Finset.univ i
⊢ 0 ≤ HPow.hPow (β := ℕ) (w.ofLp i) 2

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
ι : Type u_2
inst : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
⊢ LE.le (α := ℝ) 0 (∑ x : ι, HPow.hPow (β := ℕ) (w.ofLp x) 2)

Tactic:
exact Finset.sum_nonneg (fun i _hi ↦ by positivity)

Premises used: Finset.sum_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
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))
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))
⊢ (@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))

Tactic:
rw [← e.measurePreserving.integral_comp e.toHomeomorph.measurableEmbedding]

Premises used: LinearIsometryEquiv.toHomeomorph, MeasureTheory.MeasurePreserving.integral_comp, Homeomorph.measurableEmbedding, LinearIsometryEquiv.measurePreserving
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
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 : EuclideanSpace ℝ (Fin (Module.finrank ℝ V))) ↦
      cexp
        (-b * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2 +
          c * (↑⟪(e.symm : (a : V) → EuclideanSpace ℝ (Fin (Module.finrank ℝ V))) w, v⟫ : ℂ))) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card (Fin (Module.finrank ℝ V))) : ℂ) 2 *
      cexp
        (HPow.hPow (β := ℕ) c 2 *
            HPow.hPow (β := ℕ)
              (↑(Norm.norm (E := EuclideanSpace ℝ (Fin (Module.finrank ℝ V)))
                    ((e.symm : (a : V) → EuclideanSpace ℝ (Fin (Module.finrank ℝ V))) w :
                      EuclideanSpace ℝ (Fin (Module.finrank ℝ V)))) :
                ℂ)
              2 /
          (4 * b))

Tactic:
integral_cexp_neg_mul_sq_norm_add_of_euclideanSpace hb c (e.symm w)

Premises used: GaussianFourier.integral_cexp_neg_mul_sq_norm_add_of_euclideanSpace, LinearIsometryEquiv.symm, DFunLike.coe
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
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))
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)))
⊢ (@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:
convert! integral_cexp_neg_mul_sq_norm_add_of_euclideanSpace hb c (e.symm w)

Premises used: GaussianFourier.integral_cexp_neg_mul_sq_norm_add_of_euclideanSpace, LinearIsometryEquiv.symm, DFunLike.coe
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
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))
x : EuclideanSpace ℝ (Fin (Module.finrank ℝ V))
⊢ Norm.norm (E := V) ((e : (a : EuclideanSpace ℝ (Fin (Module.finrank ℝ V))) → V) x : V) = ‖x‖

Tactic:
simp [LinearIsometryEquiv.inner_map_eq_flip]

Premises used: LinearIsometryEquiv.inner_map_eq_flip
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
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))
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:
simp [LinearIsometryEquiv.inner_map_eq_flip]

Premises used: LinearIsometryEquiv.inner_map_eq_flip
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
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))
⊢ Module.finrank ℝ V = Fintype.card (Fin (Module.finrank ℝ V))

Tactic:
simp [LinearIsometryEquiv.inner_map_eq_flip]

Premises used: LinearIsometryEquiv.inner_map_eq_flip
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
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))
⊢ ‖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:
simp [LinearIsometryEquiv.inner_map_eq_flip]

Premises used: LinearIsometryEquiv.inner_map_eq_flip
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
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
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2)) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Module.finrank ℝ V) : ℂ) 2

Tactic:
simpa using integral_cexp_neg_mul_sq_norm_add hb 0 (0 : V)

Premises used: GaussianFourier.integral_cexp_neg_mul_sq_norm_add, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
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
rw :
  (↑(@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦ rexp (-b * HPow.hPow (β := ℕ) ‖v‖ 2)) : ℂ) =
    (↑((π / b) ^ HDiv.hDiv (α := ℝ) (↑(Module.finrank ℝ V) : ℝ) 2) : ℂ)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦ rexp (-b * HPow.hPow (β := ℕ) ‖v‖ 2)) =
    (π / b) ^ HDiv.hDiv (α := ℝ) (↑(Module.finrank ℝ V) : ℝ) 2

Tactic:
rw [← ofReal_inj]

Premises used: Complex.ofReal_inj
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
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) ↦
      cexp (-(↑b : ℂ) * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2)) =
    ((↑π : ℂ) / (↑b : ℂ)) ^ HDiv.hDiv (α := ℂ) (↑(Module.finrank ℝ V) : ℂ) 2

Tactic:
integral_cexp_neg_mul_sq_norm (show 0 < (b : ℂ).re from hb) (V := V)

Premises used: GaussianFourier.integral_cexp_neg_mul_sq_norm
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
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)
h₁ :
  (↑((π / b) ^ HDiv.hDiv (α := ℝ) (↑(Module.finrank ℝ V) : ℝ) 2) : ℂ) =
    ((↑π : ℂ) / (↑b : ℂ)) ^ HDiv.hDiv (α := ℂ) (↑(Module.finrank ℝ V) : ℂ) 2
⊢ (↑(@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦ rexp (-b * HPow.hPow (β := ℕ) ‖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)

Premises used: GaussianFourier.integral_cexp_neg_mul_sq_norm
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
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 :
  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))
⊢ 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) :
      ℂ)

Tactic:
rw [← ofRealLI.integral_comp_comm]

Premises used: LinearIsometry.integral_comp_comm, Complex.ofRealLI
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
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 (α := ℂ)
    (@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:
simp [ofRealLI]

Premises used: Complex.ofRealLI
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
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
⊢ 0 ≤ π / b

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
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 :
  (↑(π / b) : ℂ) ^ (↑(HDiv.hDiv (α := ℝ) (↑(Module.finrank ℝ V) : ℝ) 2) : ℂ) =
    (↑(π / b) : ℂ) ^ HDiv.hDiv (α := ℂ) (↑(Module.finrank ℝ V) : ℂ) 2
⊢ (↑((π / b) ^ HDiv.hDiv (α := ℝ) (↑(Module.finrank ℝ V) : ℝ) 2) : ℂ) =
    ((↑π : ℂ) / (↑b : ℂ)) ^ HDiv.hDiv (α := ℂ) (↑(Module.finrank ℝ V) : ℂ) 2

Tactic:
rw [← ofReal_div, ofReal_cpow (by positivity)]

Premises used: Complex.ofReal_cpow, Complex.ofReal_div
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
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

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
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
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)
⊢ 𝓕 (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)

Tactic:
simp only [neg_mul, fourier_eq', ofReal_neg, ofReal_mul, ofReal_ofNat,
    smul_eq_mul, ← Complex.exp_add, real_inner_comm w]

Premises used: Complex.exp_add, Complex.ofReal_neg, neg_mul, smul_eq_mul, Complex.ofReal_ofNat, real_inner_comm, Real.fourier_eq', Complex.ofReal_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
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 (-b * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪x - w, v⟫ : ℂ))) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Module.finrank ℝ V) : ℂ) 2 *
      cexp (HPow.hPow (β := ℕ) (2 * (↑π : ℂ) * I) 2 * HPow.hPow (β := ℕ) (↑‖x - w‖ : ℂ) 2 / (4 * b))

Tactic:
integral_cexp_neg_mul_sq_norm_add hb (2 * π * Complex.I) (x - w)

Premises used: Real.pi, HMul.hMul, GaussianFourier.integral_cexp_neg_mul_sq_norm_add, HSub.hSub, Complex.ofReal, OfNat.ofNat, Complex.I
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
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⟫ : ℂ))
h₁ :
  -(HPow.hPow (β := ℕ) (↑π : ℂ) 2 * HPow.hPow (β := ℕ) (↑‖x - w‖ : ℂ) 2) / b =
    HPow.hPow (β := ℕ) (2 * (↑π : ℂ) * I) 2 * HPow.hPow (β := ℕ) (↑‖x - w‖ : ℂ) 2 / (4 * b)
⊢ (@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:
convert! integral_cexp_neg_mul_sq_norm_add hb (2 * π * Complex.I) (x - w) using 3 with v

Premises used: Real.pi, HMul.hMul, GaussianFourier.integral_cexp_neg_mul_sq_norm_add, HSub.hSub, Complex.ofReal, OfNat.ofNat, Complex.I
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
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
h :
  -(2 * (↑π : ℂ) * (↑⟪w, v⟫ : ℂ) * I) + (-(b * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2) + 2 * (↑π : ℂ) * I * (↑⟪x, v⟫ : ℂ)) =
    -b * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪x - w, 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:
congr 1
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
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
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⟫ : ℂ))
⊢ -(2 * (↑π : ℂ) * (↑⟪w, v⟫ : ℂ) * I) + (-(b * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2) + 2 * (↑π : ℂ) * I * (↑⟪x, v⟫ : ℂ)) =
    -b * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2 + 2 * (↑π : ℂ) * I * (↑⟪x - w, v⟫ : ℂ)

Tactic:
simp [inner_sub_left]

Premises used: inner_sub_left
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
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, v⟫ : ℂ) - (↑⟪w, v⟫ : ℂ))

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
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
contrapose! : ∀ (hb : b = 0), b.re ≤ 0
⊢ b ≠ 0

Tactic:
contrapose! hb
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
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
rw₁ rw₂ : LE.le (α := ℝ) 0 0
⊢ b.re ≤ 0

Tactic:
rw [hb, zero_re]

Premises used: Complex.zero_re
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
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

Tactic:
have : b ≠ 0 := by contrapose! hb; rw [hb, zero_re]
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
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
h :
  -(HPow.hPow (β := ℕ) (↑π : ℂ) 2 * HPow.hPow (β := ℕ) (↑‖x - w‖ : ℂ) 2) / b =
    -(HPow.hPow (α := ℂ) (β := ℕ) 2 2 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 * HPow.hPow (β := ℕ) (↑‖x - w‖ : ℂ) 2) / (4 * b)
⊢ -(HPow.hPow (β := ℕ) (↑π : ℂ) 2 * HPow.hPow (β := ℕ) (↑‖x - w‖ : ℂ) 2) / b =
    HPow.hPow (β := ℕ) (2 * (↑π : ℂ) * I) 2 * HPow.hPow (β := ℕ) (↑‖x - w‖ : ℂ) 2 / (4 * b)

Tactic:
simp [mul_pow]

Premises used: mul_pow
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
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 2 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 * HPow.hPow (β := ℕ) (↑‖x - w‖ : ℂ) 2) / (4 * b)

Tactic:
ring