Fourier analysis

Fourier series of locally integrable periodic real-valued functions

TheoremRiemann-Lebesgue lemma (Measures and integral calculus)#

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

tendsto_integral_exp_smul_cocompact.{u_1, u_2} {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E]
  [NormedSpace ℂ E] (f : V → E) [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V]
  [T2Space V] [MeasurableSpace V] [BorelSpace V] [_root_.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)

Sources

Mathlibtendsto_integral_exp_smul_cocompact

Uses 16

Statement usesAssociative algebra over a commutative ring · Bochner integral · Borel sigma-algebra · Carathéodory's theorem (measure theory) · Compactness in terms of filters · Cos (extension of trigonometric functions to the complex plane) · Dual of a normed space · Finite-dimensionality · Hausdorff space · Measurable function · Topological module

Proof usesDominated convergence theorem · Fréchet-Riesz representation of the dual of a Hilbert space · Homeomorphisms · Pointwise convergence · Riemann-Lebesgue lemma (Analysis)

DefinitionFourier transform on \(\mathrm{L}^2(\R^d)\)#

The Fourier transform on L2 as a linear isometry equivalence.

MeasureTheory.Lp.fourierTransformₗᵢ.{u_1, u_2} (E : Type u_1) (F : Type u_2) [NormedAddCommGroup E]
  [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [InnerProductSpace ℂ F]
  [CompleteSpace F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] :
  ↥(MeasureTheory.Lp F 2 MeasureTheory.volume) ≃ₗᵢ[ℂ] ↥(MeasureTheory.Lp F 2 MeasureTheory.volume)

Sources

MathlibMeasureTheory.Lp.fourierTransformₗᵢ

Uses 12

Statement uses\(L^p\) space · Borel sigma-algebra · Complex number · Extension by continuity · Finite-dimensionality · Inner product space, over \(R\) or \(C\) · Kernel of a linear map · Lebesgue measure (Measure theory) · Quotient space (Fundamentals) · Range of a linear map · Schwartz space · Vector-valued integrable function (Bochner integral)

TheoremPlancherel’s theorem #

Plancherel's theorem for Schwartz functions.

SchwartzMap.integral_inner_fourier_fourier.{u_3, u_4} {V : Type u_3} [NormedAddCommGroup V]
  [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {H : Type u_4}
  [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (f g : SchwartzMap V H) :
  ∫ (ξ : V), inner ℂ ((FourierTransform.fourier f) ξ) ((FourierTransform.fourier g) ξ) =
    ∫ (x : V), inner ℂ (f x) (g x)