Theorems · Definition · harmonic analysis

Real.Lp.fourierTransformCLM

(V : Type u_1) →
  (E : Type u_3) →
    [inst : NormedAddCommGroup E] →
      [inst_1 : 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) →L[ℂ] BoundedContinuousFunction V E

The Fourier transform from L1 functions to bounded continuous functions as a continuous linear map.

Defined in

Mathlib.Analysis.Fourier.FourierTransform

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupInnerProductSpaceMeasurableSpaceBorelSpaceFiniteDimensional