-- Mathlib/Analysis/Fourier/Inversion.lean
lemma tendsto_integral_cexp_sq_smul (hf : Integrable f) :
    Tendsto (fun (c : ℝ) ↦ (∫ v : V, cexp (- c⁻¹ * ‖v‖^2) • f v))
      atTop (𝓝 (∫ v : V, f v))

Proof state:
case h.h.h
V : Type u_1
E : Type u_2
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : InnerProductSpace ℝ V
inst✝⁴ : MeasurableSpace V
inst✝³ : BorelSpace V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : V → E
hf : Integrable f volume
c : ℝ
hc : 0 ≤ c
v : V
⊢ 0 ≤ c⁻¹ * ‖v‖ ^ 2

Tactic:
positivity

Result:
no goals

Proof state:
case h
V : Type u_1
E : Type u_2
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : InnerProductSpace ℝ V
inst✝⁴ : MeasurableSpace V
inst✝³ : BorelSpace V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : V → E
hf : Integrable f volume
v : V
⊢ Tendsto (fun n => cexp (-↑n⁻¹ * ↑‖v‖ ^ 2) • f v) atTop (𝓝 (f v))

Tactic:
nth_rewrite 2 [show f v = cexp (- (0 : ℝ) * ‖v‖^2) • f v by simp]

Result:
case h
V : Type u_1
E : Type u_2
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : InnerProductSpace ℝ V
inst✝⁴ : MeasurableSpace V
inst✝³ : BorelSpace V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : V → E
hf : Integrable f volume
v : V
⊢ Tendsto (fun n => cexp (-↑n⁻¹ * ↑‖v‖ ^ 2) • f v) atTop (𝓝 (cexp (-↑0 * ↑‖v‖ ^ 2) • f v))

Proof state:
case h.h
V : Type u_1
E : Type u_2
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : InnerProductSpace ℝ V
inst✝⁴ : MeasurableSpace V
inst✝³ : BorelSpace V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : V → E
hf : Integrable f volume
c : ℝ
hc : 0 ≤ c
v : V
⊢ ‖rexp (-(c⁻¹ * ‖v‖ ^ 2))‖ * ‖f v‖ ≤ ‖f v‖

Tactic:
conv_rhs => rw [← one_mul (‖f v‖)]

Result:
case h.h
V : Type u_1
E : Type u_2
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : InnerProductSpace ℝ V
inst✝⁴ : MeasurableSpace V
inst✝³ : BorelSpace V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : V → E
hf : Integrable f volume
c : ℝ
hc : 0 ≤ c
v : V
⊢ ‖rexp (-(c⁻¹ * ‖v‖ ^ 2))‖ * ‖f v‖ ≤ 1 * ‖f v‖

Proof state:
V : Type u_1
E : Type u_2
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : InnerProductSpace ℝ V
inst✝⁴ : MeasurableSpace V
inst✝³ : BorelSpace V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : V → E
hf : Integrable f volume
c : ℝ
⊢ Continuous fun a => cexp (-↑c⁻¹ * ↑‖a‖ ^ 2)

Tactic:
fun_prop

Result:
no goals

Proof state:
case h
V : Type u_1
E : Type u_2
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : InnerProductSpace ℝ V
inst✝⁴ : MeasurableSpace V
inst✝³ : BorelSpace V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : V → E
hf : Integrable f volume
v : V
⊢ Tendsto (fun n => cexp (-↑n⁻¹ * ↑‖v‖ ^ 2) • f v) atTop (𝓝 (cexp (-↑0 * ↑‖v‖ ^ 2) • f v))

Tactic:
apply (Tendsto.cexp _).smul_const

Result:
V : Type u_1
E : Type u_2
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : InnerProductSpace ℝ V
inst✝⁴ : MeasurableSpace V
inst✝³ : BorelSpace V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : V → E
hf : Integrable f volume
v : V
⊢ Tendsto (fun x => -↑x⁻¹ * ↑‖v‖ ^ 2) atTop (𝓝 (-↑0 * ↑‖v‖ ^ 2))

Proof state:
case h
V : Type u_1
E : Type u_2
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : InnerProductSpace ℝ V
inst✝⁴ : MeasurableSpace V
inst✝³ : BorelSpace V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : V → E
hf : Integrable f volume
c : ℝ
hc : 0 ≤ c
⊢ ∀ᵐ (a : V), ‖cexp (-↑c⁻¹ * ↑‖a‖ ^ 2) • f a‖ ≤ ‖f a‖

Tactic:
filter_upwards with v

Result:
case h.h
V : Type u_1
E : Type u_2
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : InnerProductSpace ℝ V
inst✝⁴ : MeasurableSpace V
inst✝³ : BorelSpace V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : V → E
hf : Integrable f volume
c : ℝ
hc : 0 ≤ c
v : V
⊢ ‖cexp (-↑c⁻¹ * ↑‖v‖ ^ 2) • f v‖ ≤ ‖f v‖

Proof state:
V : Type u_1
E : Type u_2
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : InnerProductSpace ℝ V
inst✝⁴ : MeasurableSpace V
inst✝³ : BorelSpace V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : V → E
hf : Integrable f volume
⊢ Tendsto (fun c => ∫ (v : V), cexp (-↑c⁻¹ * ↑‖v‖ ^ 2) • f v) atTop (𝓝 (∫ (v : V), f v))

Tactic:
apply tendsto_integral_filter_of_dominated_convergence _ _ _ hf.norm

Result:
V : Type u_1
E : Type u_2
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : InnerProductSpace ℝ V
inst✝⁴ : MeasurableSpace V
inst✝³ : BorelSpace V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : V → E
hf : Integrable f volume
⊢ ∀ᵐ (a : V), Tendsto (fun n => cexp (-↑n⁻¹ * ↑‖a‖ ^ 2) • f a) atTop (𝓝 (f a))

V : Type u_1
E : Type u_2
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : InnerProductSpace ℝ V
inst✝⁴ : MeasurableSpace V
inst✝³ : BorelSpace V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : V → E
hf : Integrable f volume
⊢ ∀ᶠ (n : ℝ) in atTop, AEStronglyMeasurable (fun a => cexp (-↑n⁻¹ * ↑‖a‖ ^ 2) • f a) volume

V : Type u_1
E : Type u_2
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : InnerProductSpace ℝ V
inst✝⁴ : MeasurableSpace V
inst✝³ : BorelSpace V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : V → E
hf : Integrable f volume
⊢ ∀ᶠ (n : ℝ) in atTop, ∀ᵐ (a : V), ‖cexp (-↑n⁻¹ * ↑‖a‖ ^ 2) • f a‖ ≤ ‖f a‖

Proof state:
V : Type u_1
E : Type u_2
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : InnerProductSpace ℝ V
inst✝⁴ : MeasurableSpace V
inst✝³ : BorelSpace V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : V → E
hf : Integrable f volume
⊢ ∀ᶠ (n : ℝ) in atTop, AEStronglyMeasurable (fun a => cexp (-↑n⁻¹ * ↑‖a‖ ^ 2) • f a) volume

Tactic:
filter_upwards with c using
  AEStronglyMeasurable.smul (Continuous.aestronglyMeasurable (by fun_prop)) hf.1

Result:
no goals

Proof state:
case h.h
V : Type u_1
E : Type u_2
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : InnerProductSpace ℝ V
inst✝⁴ : MeasurableSpace V
inst✝³ : BorelSpace V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : V → E
hf : Integrable f volume
c : ℝ
hc : 0 ≤ c
v : V
⊢ ‖cexp (-↑c⁻¹ * ↑‖v‖ ^ 2) • f v‖ ≤ ‖f v‖

Tactic:
simp only [ofReal_inv, neg_mul, norm_smul]

Result:
case h.h
V : Type u_1
E : Type u_2
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : InnerProductSpace ℝ V
inst✝⁴ : MeasurableSpace V
inst✝³ : BorelSpace V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : V → E
hf : Integrable f volume
c : ℝ
hc : 0 ≤ c
v : V
⊢ ‖cexp (-((↑c)⁻¹ * ↑‖v‖ ^ 2))‖ * ‖f v‖ ≤ ‖f v‖

Proof state:
case h.h
V : Type u_1
E : Type u_2
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : InnerProductSpace ℝ V
inst✝⁴ : MeasurableSpace V
inst✝³ : BorelSpace V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : V → E
hf : Integrable f volume
c : ℝ
hc : 0 ≤ c
v : V
⊢ ‖cexp (-((↑c)⁻¹ * ↑‖v‖ ^ 2))‖ * ‖f v‖ ≤ ‖f v‖

Tactic:
norm_cast

Result:
case h.h
V : Type u_1
E : Type u_2
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : InnerProductSpace ℝ V
inst✝⁴ : MeasurableSpace V
inst✝³ : BorelSpace V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : V → E
hf : Integrable f volume
c : ℝ
hc : 0 ≤ c
v : V
⊢ ‖rexp (-(c⁻¹ * ‖v‖ ^ 2))‖ * ‖f v‖ ≤ ‖f v‖

Proof state:
V : Type u_1
E : Type u_2
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : InnerProductSpace ℝ V
inst✝⁴ : MeasurableSpace V
inst✝³ : BorelSpace V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : V → E
hf : Integrable f volume
v : V
⊢ f v = cexp (-↑0 * ↑‖v‖ ^ 2) • f v

Tactic:
simp

Result:
no goals