Theorems · Theorem · harmonic analysis

tendsto_integral_exp_inner_smul_cocompact_of_continuous_compact_support

∀ {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],
  Continuous f →
    HasCompactSupport f →
      Filter.Tendsto (fun w => ∫ (v : V), Real.fourierChar (-inner ℝ v w) • f v) (Filter.cocompact V) (nhds 0)

Riemann-Lebesgue Lemma for continuous and compactly-supported functions: the integral ∫ v, exp (-2 * π * ⟪w, v⟫ * I) • f v tends to 0 w.r.t. cocompact V. Note that this is primarily of interest as a preparatory step for the more general result tendsto_integral_exp_inner_smul_cocompact in which f can be arbitrary.

Defined in

Mathlib.Analysis.Fourier.RiemannLebesgueLemma

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupMeasurableSpaceBorelSpaceInnerProductSpaceFiniteDimensional