Theorems · Theorem · harmonic analysis

Real.tendsto_integral_gaussian_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} [CompleteSpace E],
  MeasureTheory.Integrable f MeasureTheory.volume →
    MeasureTheory.Integrable (FourierTransform.fourier f) MeasureTheory.volume →
      ∀ (v : V),
        Filter.Tendsto
          (fun c =>
            ∫ (w : V),
              ((↑Real.pi * ↑c) ^ (↑(Module.finrank ℝ V) / 2) * Complex.exp (-↑Real.pi ^ 2 * ↑c * ↑‖v - w‖ ^ 2)) • f w)
          Filter.atTop (nhds (FourierTransformInv.fourierInv (FourierTransform.fourier f) v))

Defined in

Mathlib.Analysis.Fourier.Inversion

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceMeasurableSpaceBorelSpaceFiniteDimensionalNormedAddCommGroupNormedSpaceCompleteSpace