Tempered distributions

InstanceDerivation of tempered distributions#

The partial derivative (or directional derivative) in the direction m : E as a continuous linear map on tempered distributions.

TemperedDistribution.instLineDeriv.{u_3, u_4} {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E]
  [NormedSpace ℝ E] [AddCommGroup F] [_root_.Module ℂ F] [TopologicalSpace F]
  [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] :
  LineDeriv E (TemperedDistribution E F) (TemperedDistribution E F)
Sources
MathlibTemperedDistribution.instLineDeriv
Uses 1
Statement usesTempered distributions

DefinitionMultiplication by a function \(C^\infty\) of slow growth#

Multiplication with a temperate growth function as a continuous linear map on 𝓢'(E, F).

TemperedDistribution.smulLeftCLM.{u_3, u_4} {E : Type u_3} (F : Type u_4) [NormedAddCommGroup E]
  [NormedSpace ℝ E] [AddCommGroup F] [_root_.Module ℂ F] [TopologicalSpace F]
  [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] (g : E → ℂ) :
  TemperedDistribution E F →L[ℂ] TemperedDistribution E F
Sources
MathlibTemperedDistribution.smulLeftCLM
Uses 3
Statement usesAlgebra of endomorphisms of a vector space · Stability by multiplication by a slowly growing smooth function · Tempered distributions

Definition\(L^p\) functions#

The natural embedding of L^p into tempered distributions.

MeasureTheory.Lp.toTemperedDistributionCLM.{u_3, u_4} {E : Type u_3} (F : Type u_4)
  [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℂ F]
  [CompleteSpace F] [MeasurableSpace E] [BorelSpace E]
  (μ : MeasureTheory.Measure E := by volume_tac) [μ.HasTemperateGrowth] (p : ENNReal)
  [hp : Fact (1 ≤ p)] : ↥(MeasureTheory.Lp F p μ) →L[ℂ] TemperedDistribution E F
Sources
MathlibMeasureTheory.Lp.toTemperedDistributionCLM
Uses 7
Statement uses\(L^p\) space · Algebra of endomorphisms of a vector space · Borel sigma-algebra · Extension by continuity · Tempered distributions · Topological module · Vector-valued integrable function (Bochner integral)

DefinitionFourier transforms#

The Fourier transform as a continuous linear map.

FourierTransform.fourierCLM.{u_2, u_3, u_4} (R : Type u_2) (E : Type u_3) {F : Type u_4}
  [Semiring R] [AddCommMonoid E] [AddCommMonoid F] [_root_.Module R E] [_root_.Module R F]
  [FourierTransform E F] [FourierAdd E F] [FourierSMul R E F] [TopologicalSpace E]
  [TopologicalSpace F] [ContinuousFourier E F] : E →L[R] F
Sources
MathlibFourierTransform.fourierCLM
Uses 1 · Used by 1
Statement usesContinuous linear map
Used byConvolution of two functions of \(\mathcal{S}(\R^d)\)

DefinitionInverse Fourier transform#

The inverse Fourier transform as a continuous linear map.

FourierTransform.fourierInvCLM.{u_2, u_3, u_4} (R : Type u_2) (E : Type u_3) {F : Type u_4}
  [Semiring R] [AddCommMonoid E] [AddCommMonoid F] [_root_.Module R E] [_root_.Module R F]
  [FourierTransformInv E F] [FourierInvAdd E F] [FourierInvSMul R E F] [TopologicalSpace E]
  [TopologicalSpace F] [ContinuousFourierInv E F] : E →L[R] F
Sources
MathlibFourierTransform.fourierInvCLM
Uses 1 · Used by 1
Statement usesContinuous linear map
Used byConvolution of two functions of \(\mathcal{S}(\R^d)\)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.