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.
• 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 ∂μ

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)