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 : ι → ℂ
simp_rw :
  @Integrable ℂ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (v : ι → ℝ) ↦
      cexp (HAdd.hAdd (α := ℂ) (-∑ i : ι, b * HPow.hPow (β := ℕ) (↑(v i) : ℂ) 2) (∑ i : ι, c i * (↑(v i) : ℂ))))
    volume
⊢ @Integrable ℂ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (v : ι → ℝ) ↦ cexp (-b * ∑ i : ι, HPow.hPow (β := ℕ) (↑(v i) : ℂ) 2 + ∑ i : ι, c i * (↑(v i) : ℂ))) volume

Tactic:
simp_rw [neg_mul, Finset.mul_sum]

Premises used: Finset.mul_sum, neg_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
ι : Type u_2
inst : Fintype ι
hb : 0 < b.re
c : ι → ℂ
⊢ @Integrable ℂ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (v : ι → ℝ) ↦
      cexp (HAdd.hAdd (α := ℂ) (-∑ i : ι, b * HPow.hPow (β := ℕ) (↑(v i) : ℂ) 2) (∑ i : ι, c i * (↑(v i) : ℂ))))
    volume

Tactic:
integrable_cexp_neg_sum_mul_add (fun _ ↦ hb) c

Premises used: GaussianFourier.integrable_cexp_neg_sum_mul_add
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
ι : Type u_2
inst : Fintype ι
hb : 0 < b.re
c : ι → ℂ
⊢ @Integrable ℂ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (v : ι → ℝ) ↦
      cexp (HAdd.hAdd (α := ℂ) (-∑ i : ι, b * HPow.hPow (β := ℕ) (↑(v i) : ℂ) 2) (∑ i : ι, c i * (↑(v i) : ℂ))))
    volume

Tactic:
exact integrable_cexp_neg_sum_mul_add (fun _ ↦ hb) c

Premises used: GaussianFourier.integrable_cexp_neg_sum_mul_add
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
ι : Type u_2
inst : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
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 (ι → ℝ))
⊢ @Integrable ℂ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (v : EuclideanSpace ℝ ι) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2 + c * (↑⟪w, v⟫ : ℂ))) volume

Tactic:
rw [← (PiLp.volume_preserving_toLp ι).integrable_comp_emb
    (MeasurableEquiv.toLp 2 _).measurableEmbedding]

Premises used: MeasurableEquiv.measurableEmbedding, MeasurableEquiv.toLp, PiLp.volume_preserving_toLp, MeasureTheory.MeasurePreserving.integrable_comp_emb, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
ι : Type u_2
inst : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
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 (ι → ℝ))
⊢ @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:
simp only [neg_mul, Function.comp_def]

Premises used: Function.comp_def, neg_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
ι : Type u_2
inst : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
⊢ @Integrable ℂ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (v : ι → ℝ) ↦
      cexp (-b * ∑ i : ι, HPow.hPow (β := ℕ) (↑(v i) : ℂ) 2 + ∑ i : ι, c * (↑(w.ofLp i) : ℂ) * (↑(v i) : ℂ)))
    volume

Tactic:
integrable_cexp_neg_mul_sum_add hb (fun i ↦ c * w i)

Premises used: HMul.hMul, GaussianFourier.integrable_cexp_neg_mul_sum_add, Complex.ofReal, WithLp.ofLp
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
ι : Type u_2
inst : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
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) : ℂ)
⊢ @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:
convert! integrable_cexp_neg_mul_sum_add hb (fun i ↦ c * w i) using 3 with v

Premises used: HMul.hMul, GaussianFourier.integrable_cexp_neg_mul_sum_add, Complex.ofReal, WithLp.ofLp
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
ι : Type u_2
inst : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
v : ι → ℝ
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) : ℂ)))
⊢ -(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:
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]

Premises used: Finset.mul_sum, mul_assoc, conj_trivial, Complex.ofReal_sum, RCLike.inner_apply, EuclideanSpace.norm_eq, neg_mul, sq_abs, PiLp.inner_apply, Finset.sum_neg_distrib, Real.norm_eq_abs, Complex.ofReal_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
ι : Type u_2
inst : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
v : ι → ℝ
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) : ℂ))
⊢ -(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:
norm_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
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) : ℂ))
h₁ : LE.le (α := ℝ) 0 (∑ x : ι, HPow.hPow (β := ℕ) (v x) 2)
⊢ -(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:
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 ℝ ι
v : ι → ℝ
⊢ -(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:
simp [Finset.mul_sum, mul_comm]

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

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
ι : Type u_2
inst : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
v : ι → ℝ
⊢ LE.le (α := ℝ) 0 (∑ x : ι, HPow.hPow (β := ℕ) (v 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 :
  @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
⊢ @Integrable ℂ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (v : V) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2 + c * (↑⟪w, v⟫ : ℂ))) volume

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

Premises used: LinearIsometryEquiv.toHomeomorph, Homeomorph.measurableEmbedding, LinearIsometryEquiv.measurePreserving, MeasureTheory.MeasurePreserving.integrable_comp_emb
-- 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))
⊢ @Integrable ℂ _ _ _ MeasureSpace.toMeasurableSpace
    (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⟫ : ℂ)))
    volume

Tactic:
integrable_cexp_neg_mul_sq_norm_add_of_euclideanSpace hb c (e.symm w)

Premises used: LinearIsometryEquiv.symm, GaussianFourier.integrable_cexp_neg_mul_sq_norm_add_of_euclideanSpace, 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 :
  ∀ (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⟫ : ℂ))
⊢ @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:
convert! integrable_cexp_neg_mul_sq_norm_add_of_euclideanSpace hb c (e.symm w) with v

Premises used: LinearIsometryEquiv.symm, GaussianFourier.integrable_cexp_neg_mul_sq_norm_add_of_euclideanSpace, 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))
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:
simp only [neg_mul, Function.comp_apply, LinearIsometryEquiv.norm_map,
    LinearIsometryEquiv.symm_symm,
    LinearIsometryEquiv.inner_map_eq_flip]

Premises used: LinearIsometryEquiv.norm_map, LinearIsometryEquiv.inner_map_eq_flip, Function.comp_apply, neg_mul, LinearIsometryEquiv.symm_symm
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
ι : Type u_2
inst : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
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)))
⊢ 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)))

Tactic:
simp_rw [← Finset.sum_neg_distrib, ← Finset.sum_add_distrib, Complex.exp_sum, ← neg_mul]

Premises used: Finset.sum_add_distrib, neg_mul, Complex.exp_sum, Finset.sum_neg_distrib
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
ι : Type u_2
inst : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
rw :
  Eq (α := ℂ)
    (∏ i : ι,
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
        cexp (-b i * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + c i * (↑x : ℂ)))
    (∏ i : ι, ((↑π : ℂ) / b i) ^ (1 / 2) * cexp (HPow.hPow (β := ℕ) (c i) 2 / (4 * b i)))
⊢ 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:
rw [integral_fintype_prod_volume_eq_prod (f := fun i (v : ℝ) ↦ cexp (-b i * v ^ 2 + c i * v))]

Premises used: HMul.hMul, Complex.ofReal, HPow.hPow, HAdd.hAdd, Complex.exp, MeasureTheory.integral_fintype_prod_volume_eq_prod, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
ι : Type u_2
inst : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
e_f :
  ∀ (i : ι),
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
        cexp (-b i * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + c i * (↑x : ℂ))) =
      ((↑π : ℂ) / b i) ^ (1 / 2) * cexp (HPow.hPow (β := ℕ) (c i) 2 / (4 * b i))
⊢ Eq (α := ℂ)
    (∏ i : ι,
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
        cexp (-b i * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + c i * (↑x : ℂ)))
    (∏ i : ι, ((↑π : ℂ) / b i) ^ (1 / 2) * cexp (HPow.hPow (β := ℕ) (c i) 2 / (4 * b i)))

Tactic:
congr with i
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
ι : Type u_2
inst : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
i : ι
⊢ (-b i).re < 0

Tactic:
simpa using hb i
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
ι : Type u_2
inst : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
i : ι
⊢ (-b i).re < 0

Tactic:
have : (-b i).re < 0 := by simpa using hb i
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
ι : Type u_2
inst : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
i : ι
this : (-b i).re < 0
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
      cexp (-b i * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + c i * (↑x : ℂ) + 0)) =
    ((↑π : ℂ) / - -b i) ^ (1 / 2) * cexp (0 - HPow.hPow (β := ℕ) (c i) 2 / (4 * -b i))

Tactic:
integral_cexp_quadratic this (c i) 0

Premises used: integral_cexp_quadratic, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
ι : Type u_2
inst : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
i : ι
this : (-b i).re < 0
h :
  Eq (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
      cexp (-b i * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + c i * (↑x : ℂ)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
      cexp (-b i * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + c i * (↑x : ℂ) + 0))
h₁ :
  ((↑π : ℂ) / b i) ^ (1 / 2) * cexp (HPow.hPow (β := ℕ) (c i) 2 / (4 * b i)) =
    ((↑π : ℂ) / - -b i) ^ (1 / 2) * cexp (0 - HPow.hPow (β := ℕ) (c i) 2 / (4 * -b i))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
      cexp (-b i * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + c i * (↑x : ℂ))) =
    ((↑π : ℂ) / b i) ^ (1 / 2) * cexp (HPow.hPow (β := ℕ) (c i) 2 / (4 * b i))

Tactic:
convert! integral_cexp_quadratic this (c i) 0 using 1

Premises used: integral_cexp_quadratic, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
ι : Type u_2
inst : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
i : ι
this : (-b i).re < 0
⊢ Eq (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
      cexp (-b i * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + c i * (↑x : ℂ)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
      cexp (-b i * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + c i * (↑x : ℂ) + 0))

Tactic:
simp [div_neg]

Premises used: div_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
ι : Type u_2
inst : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
i : ι
this : (-b i).re < 0
⊢ ((↑π : ℂ) / b i) ^ (1 / 2) * cexp (HPow.hPow (β := ℕ) (c i) 2 / (4 * b i)) =
    ((↑π : ℂ) / - -b i) ^ (1 / 2) * cexp (0 - HPow.hPow (β := ℕ) (c i) 2 / (4 * -b i))

Tactic:
simp [div_neg]

Premises used: div_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
ι : Type u_2
inst : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
rw :
  (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ)) (volume : Measure (ι → ℝ)) fun (x : ι → ℝ) ↦
      cexp
        (-b * HPow.hPow (β := ℕ) (↑(Norm.norm (E := EuclideanSpace ℝ ι) (WithLp.toLp 2 x)) : ℂ) 2 +
          c * (↑⟪w, WithLp.toLp 2 x⟫ : ℂ))) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp (HPow.hPow (β := ℕ) c 2 * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 / (4 * b))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : EuclideanSpace ℝ ι) ↦
      cexp (-b * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2 + c * (↑⟪w, v⟫ : ℂ))) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp (HPow.hPow (β := ℕ) c 2 * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 / (4 * b))

Tactic:
rw [← (PiLp.volume_preserving_toLp ι).integral_comp
    (MeasurableEquiv.toLp 2 _).measurableEmbedding]

Premises used: MeasurableEquiv.measurableEmbedding, MeasureTheory.MeasurePreserving.integral_comp, MeasurableEquiv.toLp, PiLp.volume_preserving_toLp, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
ι : Type u_2
inst : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
simp :
  (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ)) (volume : Measure (ι → ℝ)) fun (x : ι → ℝ) ↦
      cexp
        (-(b * HPow.hPow (β := ℕ) (↑(Norm.norm (E := EuclideanSpace ℝ ι) (WithLp.toLp 2 x)) : ℂ) 2) +
          c * (↑⟪w, WithLp.toLp 2 x⟫ : ℂ))) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp (HPow.hPow (β := ℕ) c 2 * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 / (4 * b))
⊢ (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ)) (volume : Measure (ι → ℝ)) fun (x : ι → ℝ) ↦
      cexp
        (-b * HPow.hPow (β := ℕ) (↑(Norm.norm (E := EuclideanSpace ℝ ι) (WithLp.toLp 2 x)) : ℂ) 2 +
          c * (↑⟪w, WithLp.toLp 2 x⟫ : ℂ))) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp (HPow.hPow (β := ℕ) c 2 * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 / (4 * b))

Tactic:
simp only [neg_mul]

Premises used: neg_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
ι : Type u_2
inst : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ι → ℝ) ↦
      cexp (-b * ∑ i : ι, HPow.hPow (β := ℕ) (↑(v i) : ℂ) 2 + ∑ i : ι, c * (↑(w.ofLp i) : ℂ) * (↑(v i) : ℂ))) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c * (↑(w.ofLp i) : ℂ)) 2) / (4 * b))

Tactic:
integral_cexp_neg_mul_sum_add hb (fun i ↦ c * w i)

Premises used: HMul.hMul, Complex.ofReal, GaussianFourier.integral_cexp_neg_mul_sum_add, WithLp.ofLp
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
ι : Type u_2
inst : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
h :
  ∀ (y : ι → ℝ),
    -(b * HPow.hPow (β := ℕ) (↑(Norm.norm (E := EuclideanSpace ℝ ι) (WithLp.toLp 2 y)) : ℂ) 2) =
      -b * ∑ i : ι, HPow.hPow (β := ℕ) (↑(y i) : ℂ) 2
h₁ : ∀ (y : ι → ℝ), c * (↑⟪w, WithLp.toLp 2 y⟫ : ℂ) = ∑ i : ι, c * (↑(w.ofLp i) : ℂ) * (↑(y i) : ℂ)
h₂ : HPow.hPow (β := ℕ) c 2 * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 = ∑ i : ι, HPow.hPow (β := ℕ) (c * (↑(w.ofLp i) : ℂ)) 2
⊢ (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ)) (volume : Measure (ι → ℝ)) fun (x : ι → ℝ) ↦
      cexp
        (-(b * HPow.hPow (β := ℕ) (↑(Norm.norm (E := EuclideanSpace ℝ ι) (WithLp.toLp 2 x)) : ℂ) 2) +
          c * (↑⟪w, WithLp.toLp 2 x⟫ : ℂ))) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp (HPow.hPow (β := ℕ) c 2 * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 / (4 * b))

Tactic:
convert! integral_cexp_neg_mul_sum_add hb (fun i ↦ c * w i) using 5 with _x y

Premises used: HMul.hMul, Complex.ofReal, GaussianFourier.integral_cexp_neg_mul_sum_add, WithLp.ofLp
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
ι : Type u_2
inst : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
y : ι → ℝ
h :
  HPow.hPow (β := ℕ) (↑√(∑ x : ι, HPow.hPow (β := ℕ) (y x) 2) : ℂ) 2 = ∑ i : ι, HPow.hPow (β := ℕ) (↑(y i) : ℂ) 2 ∨
    b = 0
⊢ -(b * HPow.hPow (β := ℕ) (↑(Norm.norm (E := EuclideanSpace ℝ ι) (WithLp.toLp 2 y)) : ℂ) 2) =
    -b * ∑ i : ι, HPow.hPow (β := ℕ) (↑(y i) : ℂ) 2

Tactic:
simp only [EuclideanSpace.norm_eq, norm_eq_abs, sq_abs, neg_mul, neg_inj, mul_eq_mul_left_iff]

Premises used: mul_eq_mul_left_iff, EuclideanSpace.norm_eq, neg_inj, neg_mul, sq_abs, Real.norm_eq_abs
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
ι : Type u_2
inst : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
y : ι → ℝ
h : HPow.hPow (β := ℕ) (√(∑ x : ι, HPow.hPow (β := ℕ) (y x) 2)) 2 = ∑ i : ι, HPow.hPow (β := ℕ) (y i) 2 ∨ b = 0
⊢ HPow.hPow (β := ℕ) (↑√(∑ x : ι, HPow.hPow (β := ℕ) (y x) 2) : ℂ) 2 = ∑ i : ι, HPow.hPow (β := ℕ) (↑(y i) : ℂ) 2 ∨
    b = 0

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

Tactic:
left
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
ι : Type u_2
inst : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
y : ι → ℝ
h : LE.le (α := ℝ) 0 (∑ x : ι, HPow.hPow (β := ℕ) (y x) 2)
⊢ HPow.hPow (β := ℕ) (√(∑ x : ι, HPow.hPow (β := ℕ) (y x) 2)) 2 = ∑ i : ι, HPow.hPow (β := ℕ) (y 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 ℝ ι
y : ι → ℝ
i : ι
_hi : Membership.mem (γ := Finset ι) Finset.univ i
⊢ 0 ≤ HPow.hPow (β := ℕ) (y i) 2

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

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

Premises used: Finset.sum_nonneg