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.mulLeftCLM: Multiplication with temperate growth function as a continuous linear map.
TemperedDistribution.instLineDeriv: The directional derivative on tempered distributions.
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_2) (F : Type u_3) [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℂ F] :

Type (max u_2 u_3)

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)

Instances For

source

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.

Instances For

Embeddings into tempered distributions #

source

def MeasureTheory.Measure.toTemperedDistribution {E : Type u_2} [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 ℂ μ)

Instances For

source

@[simp]

theorem MeasureTheory.Measure.toTemperedDistribution_apply {E : Type u_2} [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 ∂μ

source

def Function.HasTemperateGrowth.toTemperedDistribution {E : Type u_2} {F : Type u_3} [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.

Instances For

source

@[simp]

theorem Function.HasTemperateGrowth.toTemperedDistribution_apply {E : Type u_2} {F : Type u_3} [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 ∂μ

source

def SchwartzMap.toTemperedDistributionCLM (E : Type u_2) (F : Type u_3) [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.

Instances For

source

@[simp]

theorem SchwartzMap.toTemperedDistributionCLM_apply_apply {E : Type u_2} {F : Type u_3} [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 ∂μ

source

instance SchwartzMap.instCoeToTemperedDistribution {E : Type u_2} {F : Type u_3} [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) }

source

theorem SchwartzMap.coe_apply {E : Type u_2} {F : Type u_3} [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

source

def MeasureTheory.Lp.toTemperedDistribution {E : Type u_2} {F : Type u_3} [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.

Instances For

source

@[simp]

theorem MeasureTheory.Lp.toTemperedDistribution_apply {E : Type u_2} {F : Type u_3} [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 ∂μ

source

instance MeasureTheory.Lp.instCoeDep {E : Type u_2} {F : Type u_3} [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 }

source

@[simp]

theorem MeasureTheory.Lp.toTemperedDistribution_toLp_eq {E : Type u_2} {F : Type u_3} [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

source

def MeasureTheory.Lp.toTemperedDistributionCLM {E : Type u_2} (F : Type u_3) [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 := ⋯ }

Instances For

source

@[simp]

theorem MeasureTheory.Lp.toTemperedDistributionCLM_apply {E : Type u_2} {F : Type u_3} [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

source

theorem MeasureTheory.Lp.ker_toTemperedDistributionCLM_eq_bot {E : Type u_2} {F : Type u_3} [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 = ⊥

Scalar multiplication with temperate growth functions #

source

def TemperedDistribution.smulLeftCLM {E : Type u_2} (F : Type u_3) [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℂ F] (g : E → ℂ) :

TemperedDistribution E F →L[ℂ ] TemperedDistribution E F

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

Equations

TemperedDistribution.smulLeftCLM F g = PointwiseConvergenceCLM.precomp F (SchwartzMap.smulLeftCLM ℂ g)

Instances For

source

@[simp]

theorem TemperedDistribution.smulLeftCLM_apply_apply {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℂ F] (g : E → ℂ) (f : TemperedDistribution E F) (f' : SchwartzMap E ℂ) :

((smulLeftCLM F g) f) f' = f ((SchwartzMap.smulLeftCLM ℂ g) f')

source

@[simp]

theorem TemperedDistribution.smulLeftCLM_const {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℂ F] (c : ℂ) (f : TemperedDistribution E F) :

(smulLeftCLM F fun (x : E) => c) f = c • f

source

@[simp]

theorem TemperedDistribution.smulLeftCLM_smulLeftCLM_apply {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℂ F] {g₁ g₂ : E → ℂ} (hg₁ : Function.HasTemperateGrowth g₁) (hg₂ : Function.HasTemperateGrowth g₂) (f : TemperedDistribution E F) :

(smulLeftCLM F g₂) ((smulLeftCLM F g₁) f) = (smulLeftCLM F (g₁ * g₂)) f

source

theorem TemperedDistribution.smulLeftCLM_compL_smulLeftCLM {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℂ F] {g₁ g₂ : E → ℂ} (hg₁ : Function.HasTemperateGrowth g₁) (hg₂ : Function.HasTemperateGrowth g₂) :

(smulLeftCLM F g₂).comp (smulLeftCLM F g₁) = smulLeftCLM F (g₁ * g₂)

Derivatives #

source

def TemperedDistribution.derivCLM (F : Type u_3) [NormedAddCommGroup F] [NormedSpace ℂ F] :

TemperedDistribution ℝ F →L[ℂ ] TemperedDistribution ℝ F

The 1-dimensional derivative on tempered distribution as a continuous ℂ-linear map.

Equations

TemperedDistribution.derivCLM F = PointwiseConvergenceCLM.precomp F (-SchwartzMap.derivCLM ℂ ℂ)

Instances For

source

@[simp]

theorem TemperedDistribution.derivCLM_apply_apply {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℂ F] (f : TemperedDistribution ℝ F) (g : SchwartzMap ℝ ℂ) :

((derivCLM F) f) g = f (-(SchwartzMap.derivCLM ℂ ℂ) g)

source

theorem TemperedDistribution.derivCLM_toTemperedDistributionCLM_eq (𝕜 : Type u_1) {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℂ F] [RCLike 𝕜] [NormedSpace 𝕜 F] (f : SchwartzMap ℝ F) :

(derivCLM F) ((SchwartzMap.toTemperedDistributionCLM ℝ F MeasureTheory.volume) f) = (SchwartzMap.toTemperedDistributionCLM ℝ F MeasureTheory.volume) ((SchwartzMap.derivCLM 𝕜 F) f)

source

instance TemperedDistribution.instLineDeriv {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℂ F] :

LineDeriv E (TemperedDistribution E F) (TemperedDistribution E F)

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

Equations

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

source

instance TemperedDistribution.instLineDerivAdd {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℂ F] :

LineDerivAdd E (TemperedDistribution E F) (TemperedDistribution E F)

source

instance TemperedDistribution.instLineDerivSMul {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℂ F] :

LineDerivSMul ℂ E (TemperedDistribution E F) (TemperedDistribution E F)

source

instance TemperedDistribution.instContinuousLineDeriv {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℂ F] :

ContinuousLineDeriv E (TemperedDistribution E F) (TemperedDistribution E F)

source

theorem TemperedDistribution.lineDerivOpCLM_eq {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℂ F] (m : E) :

LineDeriv.lineDerivOpCLM ℂ (TemperedDistribution E F) m = PointwiseConvergenceCLM.precomp F (-LineDeriv.lineDerivOpCLM ℂ (SchwartzMap E ℂ) m)

source

@[simp]

theorem TemperedDistribution.lineDerivOp_apply_apply {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℂ F] (f : TemperedDistribution E F) (g : SchwartzMap E ℂ) (m : E) :

(LineDeriv.lineDerivOp m f) g = f (-LineDeriv.lineDerivOp m g)

source

theorem TemperedDistribution.lineDerivOp_toTemperedDistributionCLM_eq {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℂ F] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [FiniteDimensional ℝ E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] (f : SchwartzMap E F) (m : E) :

LineDeriv.lineDerivOp m ((SchwartzMap.toTemperedDistributionCLM E F μ) f) = (SchwartzMap.toTemperedDistributionCLM E F μ) (LineDeriv.lineDerivOp m f)

Fourier transform #

source

def TemperedDistribution.fourierTransformCLM (E : Type u_2) (F : Type u_3) [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 ℂ)

Instances For

source

instance TemperedDistribution.instFourierTransform {E : Type u_2} {F : Type u_3} [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) }

source

@[simp]

theorem TemperedDistribution.fourierTransformCLM_apply {E : Type u_2} {F : Type u_3} [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

source

@[simp]

theorem TemperedDistribution.fourierTransform_apply {E : Type u_2} {F : Type u_3} [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)

source

def TemperedDistribution.fourierTransformInvCLM (E : Type u_2) (F : Type u_3) [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

Instances For

source

instance TemperedDistribution.instFourierTransformInv {E : Type u_2} {F : Type u_3} [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) }

source

@[simp]

theorem TemperedDistribution.fourierTransformInvCLM_apply {E : Type u_2} {F : Type u_3} [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

source

@[simp]

theorem TemperedDistribution.fourierTransformInv_apply {E : Type u_2} {F : Type u_3} [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)

source

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

FourierPair (TemperedDistribution E F) (TemperedDistribution E F)

source

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

FourierInvPair (TemperedDistribution E F) (TemperedDistribution E F)

source

theorem TemperedDistribution.fourierTransform_toTemperedDistributionCLM_eq {E : Type u_2} {F : Type u_3} [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).

source

theorem TemperedDistribution.fourierTransformInv_toTemperedDistributionCLM_eq {E : Type u_2} {F : Type u_3} [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).

source

def TemperedDistribution.delta {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (x : E) :

TemperedDistribution E ℂ

The Dirac delta distribution

Equations

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

Instances For

source

@[deprecated TemperedDistribution.delta (since := "2025-12-23")]

def SchwartzMap.delta {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (x : E) :

TemperedDistribution E ℂ

Alias of TemperedDistribution.delta.

The Dirac delta distribution

Equations

@SchwartzMap.delta = @TemperedDistribution.delta

Instances For

source

@[simp]

theorem TemperedDistribution.delta_apply {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (x : E) (f : SchwartzMap E ℂ) :

(delta x) f = f x

source

@[deprecated TemperedDistribution.delta_apply (since := "2025-12-23")]

theorem SchwartzMap.delta_apply {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (x : E) (f : SchwartzMap E ℂ) :

(TemperedDistribution.delta x) f = f x

Alias of TemperedDistribution.delta_apply.

source

@[simp]

theorem TemperedDistribution.toTemperedDistribution_dirac_eq_delta {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] (x : E) :

(MeasureTheory.Measure.dirac x).toTemperedDistribution = delta x

Dirac measure considered as a tempered distribution is the delta distribution.

source

@[deprecated TemperedDistribution.toTemperedDistribution_dirac_eq_delta (since := "2025-12-23")]

theorem SchwartzMap.integralCLM_dirac_eq_delta {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] (x : E) :

(MeasureTheory.Measure.dirac x).toTemperedDistribution = TemperedDistribution.delta x

Alias of TemperedDistribution.toTemperedDistribution_dirac_eq_delta.

Dirac measure considered as a tempered distribution is the delta distribution.

source

theorem TemperedDistribution.fourier_delta_zero {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] :

FourierTransform.fourier (delta 0) = MeasureTheory.volume.toTemperedDistribution

The Fourier transform of the delta distribution is equal to the volume.

Informally, this is usually represented as 𝓕 δ = 1.

Documentation

Mathlib.Analysis.Distribution.TemperedDistribution

TemperedDistribution #

Main definitions #

Notation #

Embeddings into tempered distributions #

Scalar multiplication with temperate growth functions #

Derivatives #

Fourier transform #