TemperedDistribution

Main definitions

• TemperedDistribution E F: The space 𝓢(E, ℂ) →L[ℂ] F equipped with the pointwise convergence topology.
• MeasureTheory.Measure.toTemperedDistribution: Every measure of temperate growth is a tempered distribution.
• MeasureTheory.Lp.toTemperedDistribution: Every Lp function is a tempered distribution.
• TemperedDistribution.fourierTransformCLM: The Fourier transform on tempered distributions.

Notation

• 𝓢'(E, F): The space of tempered distributions TemperedDistribution E F scoped in SchwartzMap

@[reducible, inline]

abbrev TemperedDistribution (E : Type u_1) (F : Type u_2) [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℂ F] : Type (max u_1 u_2)

The space of tempered distribution is the space of continuous linear maps from the Schwartz to a normed space, equipped with the topology of pointwise convergence.

Equations

• TemperedDistribution E F = (SchwartzMap E ℂ →Lₚₜ[ℂ] F)

def SchwartzMap.«term𝓢'(_,_)» : Lean.ParserDescr

The space of tempered distribution is the space of continuous linear maps from the Schwartz to a normed space, equipped with the topology of pointwise convergence.

Equations

• One or more equations did not get rendered due to their size.

Embeddings into tempered distributions

def MeasureTheory.Measure.toTemperedDistribution {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] (μ : Measure E := by volume_tac) [hμ : μ.HasTemperateGrowth] : TemperedDistribution E ℂ

Every temperate growth measure defines a tempered distribution.

Equations

• μ.toTemperedDistribution = (ContinuousLinearMap.toPointwiseConvergenceCLM ℂ (RingHom.id ℂ) (SchwartzMap E ℂ) ℂ) (SchwartzMap.integralCLM ℂ μ)

@[simp]

theorem MeasureTheory.Measure.toTemperedDistribution_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] (μ : Measure E := by volume_tac) [hμ : μ.HasTemperateGrowth] (g : SchwartzMap E ℂ) : μ.toTemperedDistribution g = ∫ (x : E), g x ∂μ

def MeasureTheory.Lp.toTemperedDistribution {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℂ F] [CompleteSpace F] [MeasurableSpace E] [BorelSpace E] {μ : Measure E} [hμ : μ.HasTemperateGrowth] {p : ENNReal} [hp : Fact (1 ≤ p)] (f : ↥(Lp F p μ)) : TemperedDistribution E F

Define a tempered distribution from a L^p function.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MeasureTheory.Lp.toTemperedDistribution_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℂ F] [CompleteSpace F] [MeasurableSpace E] [BorelSpace E] {μ : Measure E} [hμ : μ.HasTemperateGrowth] {p : ENNReal} [hp : Fact (1 ≤ p)] (f : ↥(Lp F p μ)) (g : SchwartzMap E ℂ) : (toTemperedDistribution f) g = ∫ (x : E), g x • ↑↑f x ∂μ

instance MeasureTheory.Lp.instCoeDep {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℂ F] [CompleteSpace F] [MeasurableSpace E] [BorelSpace E] {μ : Measure E} [hμ : μ.HasTemperateGrowth] {p : ENNReal} [hp : Fact (1 ≤ p)] (f : ↥(Lp F p μ)) : CoeDep (↥(Lp F p μ)) f (TemperedDistribution E F)

Equations

• MeasureTheory.Lp.instCoeDep f = { coe := MeasureTheory.Lp.toTemperedDistribution f }

def MeasureTheory.Lp.toTemperedDistributionCLM {E : Type u_1} (F : Type u_2) [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℂ F] [CompleteSpace F] [MeasurableSpace E] [BorelSpace E] (μ : Measure E := by volume_tac) [μ.HasTemperateGrowth] (p : ENNReal) [hp : Fact (1 ≤ p)] : ↥(Lp F p μ) →L[ℂ] TemperedDistribution E F

The natural embedding of L^p into tempered distributions.

Equations

• MeasureTheory.Lp.toTemperedDistributionCLM F μ p = { toFun := MeasureTheory.Lp.toTemperedDistribution, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

@[simp]

theorem MeasureTheory.Lp.toTemperedDistributionCLM_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℂ F] [CompleteSpace F] [MeasurableSpace E] [BorelSpace E] {μ : Measure E} [hμ : μ.HasTemperateGrowth] {p : ENNReal} [hp : Fact (1 ≤ p)] (f : ↥(Lp F p μ)) : (toTemperedDistributionCLM F μ p) f = toTemperedDistribution f

theorem MeasureTheory.Lp.ker_toTemperedDistributionCLM_eq_bot {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℂ F] [CompleteSpace F] [MeasurableSpace E] [BorelSpace E] {μ : Measure E} [hμ : μ.HasTemperateGrowth] [FiniteDimensional ℝ E] [IsLocallyFiniteMeasure μ] {p : ENNReal} [hp : Fact (1 ≤ p)] : LinearMap.ker (toTemperedDistributionCLM F μ p) = ⊥

Fourier transform

def TemperedDistribution.fourierTransformCLM (E : Type u_1) (F : Type u_2) [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [NormedSpace ℂ F] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] : TemperedDistribution E F →L[ℂ] TemperedDistribution E F

The Fourier transform on tempered distributions as a continuous linear map.

Equations

• TemperedDistribution.fourierTransformCLM E F = PointwiseConvergenceCLM.precomp F (SchwartzMap.fourierTransformCLM ℂ)

instance TemperedDistribution.instFourierTransform {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [NormedSpace ℂ F] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] : FourierTransform (TemperedDistribution E F) (TemperedDistribution E F)

Equations

• TemperedDistribution.instFourierTransform = { fourier := ⇑(TemperedDistribution.fourierTransformCLM E F) }

@[simp]

theorem TemperedDistribution.fourierTransformCLM_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [NormedSpace ℂ F] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (f : TemperedDistribution E F) : (fourierTransformCLM E F) f = FourierTransform.fourier f

@[simp]

theorem TemperedDistribution.fourierTransform_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [NormedSpace ℂ F] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (f : TemperedDistribution E F) (g : SchwartzMap E ℂ) : (FourierTransform.fourier f) g = f (FourierTransform.fourier g)

def TemperedDistribution.fourierTransformInvCLM (E : Type u_1) (F : Type u_2) [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [NormedSpace ℂ F] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] : TemperedDistribution E F →L[ℂ] TemperedDistribution E F

The inverse Fourier transform on tempered distributions as a continuous linear map.

Equations

• TemperedDistribution.fourierTransformInvCLM E F = PointwiseConvergenceCLM.precomp F ↑(SchwartzMap.fourierTransformCLE ℂ).symm

instance TemperedDistribution.instFourierTransformInv {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [NormedSpace ℂ F] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] : FourierTransformInv (TemperedDistribution E F) (TemperedDistribution E F)

Equations

• TemperedDistribution.instFourierTransformInv = { fourierInv := ⇑(TemperedDistribution.fourierTransformInvCLM E F) }

@[simp]

theorem TemperedDistribution.fourierTransformInvCLM_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [NormedSpace ℂ F] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (f : TemperedDistribution E F) : (fourierTransformInvCLM E F) f = FourierTransformInv.fourierInv f

@[simp]

theorem TemperedDistribution.fourierTransformInv_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [NormedSpace ℂ F] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (f : TemperedDistribution E F) (g : SchwartzMap E ℂ) : (FourierTransformInv.fourierInv f) g = f (FourierTransformInv.fourierInv g)

instance TemperedDistribution.instFourierPair {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [NormedSpace ℂ F] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] : FourierPair (TemperedDistribution E F) (TemperedDistribution E F)

instance TemperedDistribution.instFourierPairInv {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [NormedSpace ℂ F] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] : FourierInvPair (TemperedDistribution E F) (TemperedDistribution E F)