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.
• Function.HasTemperateGrowth.toTemperedDistribution: Every function of temperate growth is a tempered distribution.
• SchwartzMap.toTemperedDistributionCLM: The canonical map from 𝓢 to 𝓢' as a continuous linear map.
• 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 Function.HasTemperateGrowth.toTemperedDistribution {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℂ F] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] (μ : MeasureTheory.Measure E := by volume_tac) [hμ : μ.HasTemperateGrowth] {f : E → F} (hf : HasTemperateGrowth f) : TemperedDistribution E F

A function of temperate growth f defines a tempered distribution via integration, namely g ↦ ∫ (x : E), g x • f x ∂μ.

Equations

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

@[simp]

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

def SchwartzMap.toTemperedDistributionCLM (E : Type u_1) (F : Type u_2) [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℂ F] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] (μ : MeasureTheory.Measure E := by volume_tac) [hμ : μ.HasTemperateGrowth] : SchwartzMap E F →L[ℂ] TemperedDistribution E F

The canonical embedding of 𝓢(E, F) into 𝓢'(E, F) as a continuous linear map.

Equations

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

@[simp]

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

instance SchwartzMap.instCoeToTemperedDistribution {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℂ F] [MeasureTheory.MeasureSpace E] [BorelSpace E] [SecondCountableTopology E] [MeasureTheory.volume.HasTemperateGrowth] : Coe (SchwartzMap E F) (TemperedDistribution E F)

Equations

• SchwartzMap.instCoeToTemperedDistribution = { coe := ⇑(SchwartzMap.toTemperedDistributionCLM E F MeasureTheory.volume) }

theorem SchwartzMap.coe_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℂ F] [MeasureTheory.MeasureSpace E] [BorelSpace E] [SecondCountableTopology E] [MeasureTheory.volume.HasTemperateGrowth] (f : SchwartzMap E F) (g : SchwartzMap E ℂ) : ((toTemperedDistributionCLM E F MeasureTheory.volume) f) g = ∫ (x : E), g x • f 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 }

@[simp]

theorem MeasureTheory.Lp.toTemperedDistribution_toLp_eq {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] [SecondCountableTopology E] {p : ENNReal} [hp : Fact (1 ≤ p)] (f : SchwartzMap E F) : toTemperedDistribution (f.toLp p μ) = (SchwartzMap.toTemperedDistributionCLM E F μ) 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)] : (↑(toTemperedDistributionCLM F μ p)).ker = ⊥

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)

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

The distributional Fourier transform and the classical Fourier transform coincide on 𝓢(E, F).

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

The distributional inverse Fourier transform and the classical inverse Fourier transform coincide on 𝓢(E, F).