Theorems · Theorem · functional analysis

TemperedDistribution.MemSobolev.fourierMultiplierCLM_of_bounded

∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : FiniteDimensional ℝ E] [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E]
  [inst_6 : InnerProductSpace ℂ F] [inst_7 : CompleteSpace F] {s : ℝ} {f : TemperedDistribution E F},
  TemperedDistribution.MemSobolev s 2 f →
    ∀ {g : E → ℂ},
      Function.HasTemperateGrowth g →
        (∃ C, ∀ (x : E), ‖g x‖ ≤ C) →
          TemperedDistribution.MemSobolev s 2 ((TemperedDistribution.fourierMultiplierCLM F g) f)

The Fourier multiplier with a bounded function maps H ^ s to H ^ s.

Defined in

Mathlib.Analysis.Distribution.Sobolev

Cited by

3 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedAddCommGroupInnerProductSpaceFiniteDimensionalMeasurableSpaceBorelSpaceInnerProductSpaceCompleteSpace