Theorems · Theorem · harmonic analysis

tendsto_integral_exp_smul_cocompact

∀ {E : Type u_1} {V : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : V → E)
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [IsTopologicalAddGroup V] [T2Space V]
  [inst_6 : MeasurableSpace V] [BorelSpace V] [inst_8 : Module ℝ V] [ContinuousSMul ℝ V] [FiniteDimensional ℝ V]
  (μ : MeasureTheory.Measure V) [μ.IsAddHaarMeasure],
  Filter.Tendsto (fun w => ∫ (v : V), Real.fourierChar (-w v) • f v ∂μ) (Filter.cocompact (StrongDual ℝ V)) (nhds 0)

Riemann-Lebesgue lemma for functions on a finite-dimensional real vector space, formulated via dual space.

Defined in

Mathlib.Analysis.Fourier.RiemannLebesgueLemma

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceAddCommGroupTopologicalSpaceIsTopologicalAddGroupT2SpaceMeasurableSpaceBorelSpaceModuleContinuousSMulFiniteDimensionalMeasureTheory.Measure.IsAddHaarMeasure