-- Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean
theorem integral_cexp_neg_mul_sq_norm_add_of_euclideanSpace
    {ι : Type*} [Fintype ι] (hb : 0 < b.re) (c : ℂ) (w : EuclideanSpace ℝ ι) :
    ∫ v : EuclideanSpace ℝ ι, cexp (- b * ‖v‖^2 + c * ⟪w, v⟫) =
      (π / b) ^ (Fintype.card ι / 2 : ℂ) * cexp (c ^ 2 * ‖w‖^2 / (4 * b))

Proof state:
case h.e'_3.h.e'_6.h.e'_1.h.e'_5.e_a
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
this : MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι).symm) volume volume
⊢ √(∑ x : ι, w x ^ 2) ^ 2 = ∑ i : ι, w i ^ 2

Tactic:
rw [sq_sqrt]

Result:
case h.e'_3.h.e'_6.h.e'_1.h.e'_5.e_a
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
this : MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι).symm) volume volume
⊢ 0 ≤ ∑ x : ι, w x ^ 2

Proof state:
case h.e'_2.h.e'_7.h.h.e'_1.h.e'_5.h
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
this : MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι).symm) volume volume
y : ι → ℝ
⊢ 0 ≤ ∑ x : ι, y x ^ 2

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

Result:
no goals

Proof state:
case h.e'_2.h.e'_7.h.h.e'_1.h.e'_5
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
this : MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι).symm) volume volume
y : ι → ℝ
⊢ √(∑ x : ι, y x ^ 2) ^ 2 = ∑ i : ι, y i ^ 2 ∨ b = 0

Tactic:
left

Result:
case h.e'_2.h.e'_7.h.h.e'_1.h.e'_5.h
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
this : MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι).symm) volume volume
y : ι → ℝ
⊢ √(∑ x : ι, y x ^ 2) ^ 2 = ∑ i : ι, y i ^ 2

Proof state:
case h.e'_3.h.e'_6.h.e'_1.h.e'_5
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
this : MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι).symm) volume volume
⊢ c ^ 2 * ↑‖w‖ ^ 2 = ∑ i : ι, (c * ↑(w i)) ^ 2

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

Result:
case h.e'_3.h.e'_6.h.e'_1.h.e'_5
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
this : MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι).symm) volume volume
⊢ c ^ 2 * ↑√(∑ x : ι, w x ^ 2) ^ 2 = c ^ 2 * ∑ i : ι, ↑(w i) ^ 2

Proof state:
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
⊢ ∫ (v : EuclideanSpace ℝ ι), cexp (-b * ↑‖v‖ ^ 2 + c * ↑(inner w v)) =
    (↑π / b) ^ (↑(Fintype.card ι) / 2) * cexp (c ^ 2 * ↑‖w‖ ^ 2 / (4 * b))

Tactic:
have := (EuclideanSpace.volume_preserving_measurableEquiv ι).symm

Result:
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
this : MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι).symm) volume volume
⊢ ∫ (v : EuclideanSpace ℝ ι), cexp (-b * ↑‖v‖ ^ 2 + c * ↑(inner w v)) =
    (↑π / b) ^ (↑(Fintype.card ι) / 2) * cexp (c ^ 2 * ↑‖w‖ ^ 2 / (4 * b))

Proof state:
case h.e'_3.h.e'_6.h.e'_1.h.e'_5.e_a
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
this : MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι).symm) volume volume
⊢ ↑√(∑ x : ι, w x ^ 2) ^ 2 = ∑ i : ι, ↑(w i) ^ 2

Tactic:
norm_cast

Result:
case h.e'_3.h.e'_6.h.e'_1.h.e'_5.e_a
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
this : MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι).symm) volume volume
⊢ √(∑ x : ι, w x ^ 2) ^ 2 = ∑ i : ι, w i ^ 2

Proof state:
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
this : MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι).symm) volume volume
⊢ ∫ (v : EuclideanSpace ℝ ι), cexp (-b * ↑‖v‖ ^ 2 + c * ↑(inner w v)) =
    (↑π / b) ^ (↑(Fintype.card ι) / 2) * cexp (c ^ 2 * ↑‖w‖ ^ 2 / (4 * b))

Tactic:
rw [← this.integral_comp (MeasurableEquiv.measurableEmbedding _)]

Result:
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
this : MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι).symm) volume volume
⊢ ∫ (x : ι → ℝ),
      cexp
        (-b * ↑‖(EuclideanSpace.measurableEquiv ι).symm x‖ ^ 2 +
          c * ↑(inner w ((EuclideanSpace.measurableEquiv ι).symm x))) ∂volume =
    (↑π / b) ^ (↑(Fintype.card ι) / 2) * cexp (c ^ 2 * ↑‖w‖ ^ 2 / (4 * b))

Proof state:
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
this : MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι).symm) volume volume
i : ι
_hi : i ∈ Finset.univ
⊢ 0 ≤ w i ^ 2

Tactic:
positivity

Result:
no goals

Proof state:
case h.e'_2.h.e'_7.h.h.e'_1.h.e'_5.h
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
this : MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι).symm) volume volume
y : ι → ℝ
⊢ √(∑ x : ι, y x ^ 2) ^ 2 = ∑ i : ι, y i ^ 2

Tactic:
rw [sq_sqrt]

Result:
case h.e'_2.h.e'_7.h.h.e'_1.h.e'_5.h
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
this : MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι).symm) volume volume
y : ι → ℝ
⊢ 0 ≤ ∑ x : ι, y x ^ 2

Proof state:
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
this : MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι).symm) volume volume
⊢ ∫ (x : ι → ℝ),
      cexp
        (-(b * ↑‖(EuclideanSpace.measurableEquiv ι).symm x‖ ^ 2) +
          c * ↑(inner w ((EuclideanSpace.measurableEquiv ι).symm x))) ∂volume =
    (↑π / b) ^ (↑(Fintype.card ι) / 2) * cexp (c ^ 2 * ↑‖w‖ ^ 2 / (4 * b))

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

Result:
case h.e'_2.h.e'_7.h.h.e'_1.h.e'_5
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
this : MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι).symm) volume volume
y : ι → ℝ
⊢ -(b * ↑‖(EuclideanSpace.measurableEquiv ι).symm y‖ ^ 2) = -b * ∑ i : ι, ↑(y i) ^ 2

case h.e'_2.h.e'_7.h.h.e'_1.h.e'_6
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
this : MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι).symm) volume volume
y : ι → ℝ
⊢ c * ↑(inner w ((EuclideanSpace.measurableEquiv ι).symm y)) = ∑ i : ι, c * ↑(w i) * ↑(y i)

case h.e'_3.h.e'_6.h.e'_1.h.e'_5
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
this : MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι).symm) volume volume
⊢ c ^ 2 * ↑‖w‖ ^ 2 = ∑ i : ι, (c * ↑(w i)) ^ 2

Proof state:
case h.e'_2.h.e'_7.h.h.e'_1.h.e'_5
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
this : MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι).symm) volume volume
y : ι → ℝ
⊢ ↑√(∑ x : ι, y x ^ 2) ^ 2 = ∑ i : ι, ↑(y i) ^ 2 ∨ b = 0

Tactic:
norm_cast

Result:
case h.e'_2.h.e'_7.h.h.e'_1.h.e'_5
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
this : MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι).symm) volume volume
y : ι → ℝ
⊢ √(∑ x : ι, y x ^ 2) ^ 2 = ∑ i : ι, y i ^ 2 ∨ b = 0

Proof state:
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
this : MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι).symm) volume volume
y : ι → ℝ
i : ι
_hi : i ∈ Finset.univ
⊢ 0 ≤ y i ^ 2

Tactic:
positivity

Result:
no goals

Proof state:
case h.e'_3.h.e'_6.h.e'_1.h.e'_5.e_a
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
this : MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι).symm) volume volume
⊢ 0 ≤ ∑ x : ι, w x ^ 2

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

Result:
no goals