Theorems · Theorem · harmonic analysis

tendsto_integral_exp_inner_smul_cocompact

∀ {E : Type u_1} {V : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : V → E)
  [inst_2 : NormedAddCommGroup V] [inst_3 : MeasurableSpace V] [inst_4 : BorelSpace V] [inst_5 : InnerProductSpace ℝ V]
  [inst_6 : FiniteDimensional ℝ V],
  Filter.Tendsto (fun w => ∫ (v : V), Real.fourierChar (-inner ℝ v w) • f v) (Filter.cocompact V) (nhds 0)

Riemann-Lebesgue lemma for functions on a real inner-product space: the integral ∫ v, exp (-2 * π * ⟪w, v⟫ * I) • f v tends to 0 as w → ∞.

Defined in

Mathlib.Analysis.Fourier.RiemannLebesgueLemma

Cited by

3 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupMeasurableSpaceBorelSpaceInnerProductSpaceFiniteDimensional