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

Proof state:
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
this : MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι)) volume volume
⊢ Integrable (fun v => cexp (-b * ↑‖v‖ ^ 2 + c * ↑(inner w v))) volume

Tactic:
rw [← MeasurePreserving.integrable_comp_emb this.symm (MeasurableEquiv.measurableEmbedding _)]

Result:
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
this : MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι)) volume volume
⊢ Integrable ((fun v => cexp (-b * ↑‖v‖ ^ 2 + c * ↑(inner w v))) ∘ ⇑(EuclideanSpace.measurableEquiv ι).symm) volume

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

Tactic:
positivity

Result:
no goals

Proof state:
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
⊢ Integrable (fun v => cexp (-b * ↑‖v‖ ^ 2 + c * ↑(inner w v))) volume

Tactic:
have := EuclideanSpace.volume_preserving_measurableEquiv ι

Result:
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
this : MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι)) volume volume
⊢ Integrable (fun v => cexp (-b * ↑‖v‖ ^ 2 + c * ↑(inner w v))) volume

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

Tactic:
rw [sq_sqrt]

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

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

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

Tactic:
simp only [EuclideanSpace.measurableEquiv, MeasurableEquiv.symm_mk, MeasurableEquiv.coe_mk,
  EuclideanSpace.norm_eq, WithLp.equiv_symm_pi_apply, Real.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, add_left_inj, neg_inj]

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

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

Tactic:
simp only [neg_mul, Function.comp_def]

Result:
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
this : MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι)) volume volume
⊢ Integrable
    (fun x =>
      cexp
        (-(b * ↑‖(EuclideanSpace.measurableEquiv ι).symm x‖ ^ 2) +
          c * ↑(inner w ((EuclideanSpace.measurableEquiv ι).symm x))))
    volume

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

Tactic:
simp [Finset.mul_sum]

Result:
no goals

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

Tactic:
norm_cast

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

Proof state:
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
this : MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι)) volume volume
⊢ Integrable
    (fun x =>
      cexp
        (-(b * ↑‖(EuclideanSpace.measurableEquiv ι).symm x‖ ^ 2) +
          c * ↑(inner w ((EuclideanSpace.measurableEquiv ι).symm x))))
    volume

Tactic:
convert integrable_cexp_neg_mul_sum_add hb (fun i ↦ c * w i) using 3 with v

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

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

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

Result:
no goals