Theorems · Theorem · harmonic analysis

Fourier.fourierIntegral_comp_add_right

∀ {𝕜 : Type u_1} [inst : CommRing 𝕜] [inst_1 : MeasurableSpace 𝕜] {E : Type u_2} [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace ℂ E] [MeasurableAdd 𝕜] (e : AddChar 𝕜 Circle) (μ : MeasureTheory.Measure 𝕜)
  [μ.IsAddRightInvariant] (f : 𝕜 → E) (v₀ : 𝕜),
  Fourier.fourierIntegral e μ (f ∘ fun v => v + v₀) = fun w => e (v₀ * w) • Fourier.fourierIntegral e μ f w

The Fourier transform converts right-translation into scalar multiplication by a phase factor.

Defined in

Mathlib.Analysis.Fourier.FourierTransform

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingMeasurableSpaceNormedAddCommGroupNormedSpaceMeasurableAddMeasureTheory.Measure.IsAddRightInvariant