Theorems · Definition · functional analysis

TemperedDistribution.fourierMultiplierCLM

{E : Type u_3} →
  (F : Type u_4) →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedAddCommGroup F] →
        [inst_2 : InnerProductSpace ℝ E] →
          [inst_3 : NormedSpace ℂ F] →
            [FiniteDimensional ℝ E] →
              [inst_5 : MeasurableSpace E] →
                [BorelSpace E] → (E → ℂ) → TemperedDistribution E F →L[ℂ] TemperedDistribution E F

Fourier multiplier on tempered distributions.

Defined in

Mathlib.Analysis.Distribution.FourierMultiplier

Cited by

16 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedAddCommGroupInnerProductSpaceNormedSpaceFiniteDimensionalMeasurableSpaceBorelSpace