Theorems · Definition · harmonic analysis

Fourier.fourierIntegral

{𝕜 : Type u_1} →
  [inst : CommRing 𝕜] →
    [inst_1 : MeasurableSpace 𝕜] →
      {E : Type u_2} →
        [inst_2 : NormedAddCommGroup E] →
          [NormedSpace ℂ E] → AddChar 𝕜 Circle → MeasureTheory.Measure 𝕜 → (𝕜 → E) → 𝕜 → E

The Fourier transform integral for f : 𝕜 → E, with respect to the measure μ and additive character e.

Defined in

Mathlib.Analysis.Fourier.FourierTransform

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommRingMeasurableSpaceNormedAddCommGroupNormedSpace