Fourier analysis

TheoremFourier transform as an integral#

Mathlib states this as Real.fourier_eq.

Real.fourier_eq.{u_1, u_3} {V : Type u_1} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E]
  [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V]
  [FiniteDimensional ℝ V] (f : V → E) (w : V) :
  FourierTransform.fourier f w = ∫ (v : V), Real.fourierChar (-inner ℝ v w) • f v
Sources
MathlibReal.fourier_eq
Uses 6
Statement usesBochner integral · Borel sigma-algebra · Cos (extension of trigonometric functions to the complex plane) · Finite-dimensionality · Inner product space, over \(R\) or \(C\) · Lebesgue measure (Measure theory)

TheoremInversion formula#

Fourier inversion formula: If a function f on a finite-dimensional real inner product space is continuous, integrable, and its Fourier transform 𝓕 f is also integrable, then 𝓕⁻ (𝓕 f) = f.

Continuous.fourierInv_fourier_eq.{u_1, u_2} {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V]
  [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V]
  [NormedAddCommGroup E] [NormedSpace ℂ E] {f : V → E} [CompleteSpace E] (h : Continuous f)
  (hf : MeasureTheory.Integrable f MeasureTheory.volume)
  (h'f : MeasureTheory.Integrable (FourierTransform.fourier f) MeasureTheory.volume) :
  FourierTransformInv.fourierInv (FourierTransform.fourier f) = f
Sources
MathlibContinuous.fourierInv_fourier_eq
Uses 7 · Used by 1
Statement usesBorel sigma-algebra · Complex number · Finite-dimensionality · Inner product space, over \(R\) or \(C\) · Lebesgue measure (Measure theory) · Vector-valued integrable function (Bochner integral)
Proof usesFourier theorem
Used byPlancherel’s theorem

TheoremRiemann-Lebesgue lemma (Analysis)#

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 → ∞.

tendsto_integral_exp_inner_smul_cocompact.{u_1, u_2} {E : Type u_1} {V : Type u_2}
  [NormedAddCommGroup E] [NormedSpace ℂ E] (f : V → E) [NormedAddCommGroup V] [MeasurableSpace V]
  [BorelSpace V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] :
  Filter.Tendsto (fun w => ∫ (v : V), Real.fourierChar (-inner ℝ v w) • f v) (Filter.cocompact V)
    (nhds 0)
Sources
Mathlibtendsto_integral_exp_inner_smul_cocompact
Uses 15 · Used by 1
Statement usesBochner integral · Borel sigma-algebra · Compactness in terms of filters · Cos (extension of trigonometric functions to the complex plane) · Finite-dimensionality · Inner product space, over \(R\) or \(C\) · Lebesgue measure (Measure theory)
Proof usesCarathéodory's theorem (measure theory) · Completeness of R · Field \(\C\) of complex numbers · Heine-Borel theorem (finite-dimensional normed spaces are proper) · Measurable function · The Binomial Theorem · Uniformly continuous function · Urysohn's lemma
Used byRiemann-Lebesgue lemma (Measures and integral calculus)

TheoremParseval formula for Fourier series#

Mathlib states this as tsum_sq_fourierCoeff.

tsum_sq_fourierCoeff {T : ℝ} [hT : Fact (0 < T)]
  (f : ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)) :
  ∑' (i : ℤ), ‖fourierCoeff (↑↑f) i‖ ^ 2 = ∫ (t : AddCircle T), ‖↑↑f t‖ ^ 2 ∂AddCircle.haarAddCircle
Sources
Mathlibtsum_sq_fourierCoeff
Uses 1
Statement usesFourier Series

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.