Theorems · Theorem · harmonic analysis

Real.tendsto_integral_cexp_sq_smul

∀ {V : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
  [inst_2 : MeasurableSpace V] [inst_3 : BorelSpace V] [inst_4 : FiniteDimensional ℝ V] [inst_5 : NormedAddCommGroup E]
  [inst_6 : NormedSpace ℂ E] {f : V → E},
  MeasureTheory.Integrable f MeasureTheory.volume →
    Filter.Tendsto (fun c => ∫ (v : V), Complex.exp (-↑c⁻¹ * ↑‖v‖ ^ 2) • f v) Filter.atTop (nhds (∫ (v : V), f v))

Defined in

Mathlib.Analysis.Fourier.Inversion

Cited by

1 results in Mathlib

Foundations

Depth 253 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupInnerProductSpaceMeasurableSpaceBorelSpaceFiniteDimensionalNormedAddCommGroupNormedSpace