Theorems · Definition · harmonic analysis

Real.Lp.fourierTransform

{V : Type u_1} →
  {E : Type u_3} →
    [inst : NormedAddCommGroup E] →
      [NormedSpace ℂ E] →
        [inst_2 : NormedAddCommGroup V] →
          [inst_3 : InnerProductSpace ℝ V] →
            [inst_4 : MeasurableSpace V] →
              [inst_5 : BorelSpace V] →
                [inst_6 : FiniteDimensional ℝ V] →
                  ↥(MeasureTheory.Lp E 1 MeasureTheory.volume) → BoundedContinuousFunction V E

The Fourier transform from L1 functions to bounded continuous functions.

Defined in

Mathlib.Analysis.Fourier.FourierTransform

Cited by

5 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupInnerProductSpaceMeasurableSpaceBorelSpaceFiniteDimensional