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_3) (F : Type u_4) [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℂ F] : Type (max u_3 u_4)

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

noncomputable def MeasureTheory.Measure.toTemperedDistribution {E : Type u_3} [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_3} [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 ∂μ

noncomputable def Function.HasTemperateGrowth.toTemperedDistribution {E : Type u_3} {F : Type u_4} [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_3} {F : Type u_4} [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 ∂μ

noncomputable def SchwartzMap.toTemperedDistributionCLM (E : Type u_3) (F : Type u_4) [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_3} {F : Type u_4} [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 ∂μ

@[implicit_reducible]

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

noncomputable def MeasureTheory.Lp.toTemperedDistribution {E : Type u_3} {F : Type u_4} [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_3} {F : Type u_4} [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 ∂μ

@[implicit_reducible]

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

noncomputable def MeasureTheory.Lp.toTemperedDistributionCLM {E : Type u_3} (F : Type u_4) [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_3} {F : Type u_4} [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_3} {F : Type u_4} [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

noncomputable def TemperedDistribution.smulLeftCLM {E : Type u_3} (F : Type u_4) [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)

@[simp]

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

@[simp]

theorem TemperedDistribution.smulLeftCLM_const {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℂ F] (c : ℂ) (f : TemperedDistribution E F) : (smulLeftCLM F fun (x : E) => c) f = c • f

@[simp]

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

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

theorem TemperedDistribution.smulLeftCLM_smul {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℂ F] {g : E → ℂ} (hg : Function.HasTemperateGrowth g) (c : ℂ) : smulLeftCLM F (c • g) = c • smulLeftCLM F g

theorem TemperedDistribution.smulLeftCLM_add {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℂ F] {g₁ g₂ : E → ℂ} (hg₁ : Function.HasTemperateGrowth g₁) (hg₂ : Function.HasTemperateGrowth g₂) : smulLeftCLM F (g₁ + g₂) = smulLeftCLM F g₁ + smulLeftCLM F g₂

theorem TemperedDistribution.smulLeftCLM_sub {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℂ F] {g₁ g₂ : E → ℂ} (hg₁ : Function.HasTemperateGrowth g₁) (hg₂ : Function.HasTemperateGrowth g₂) : smulLeftCLM F (g₁ - g₂) = smulLeftCLM F g₁ - smulLeftCLM F g₂

theorem TemperedDistribution.smulLeftCLM_neg {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℂ F] {g : E → ℂ} (hg : Function.HasTemperateGrowth g) : smulLeftCLM F (-g) = -smulLeftCLM F g

theorem TemperedDistribution.smulLeftCLM_sum {ι : Type u_1} {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℂ F] {g : ι → E → ℂ} {s : Finset ι} (hg : ∀ i ∈ s, Function.HasTemperateGrowth (g i)) : (smulLeftCLM F fun (x : E) => ∑ i ∈ s, g i x) = ∑ i ∈ s, smulLeftCLM F (g i)

theorem MeasureTheory.Lp.toTemperedDistribution_smul_eq {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℂ F] [MeasurableSpace E] [BorelSpace E] {μ : Measure E} [hμ : μ.HasTemperateGrowth] [CompleteSpace F] {p q r : ENNReal} [p.HolderTriple q r] [Fact (1 ≤ q)] [Fact (1 ≤ r)] {g : E → ℂ} (hg₁ : Function.HasTemperateGrowth g) (hg₂ : MemLp g p μ) (f : ↥(Lp F q μ)) : toTemperedDistribution (MemLp.toLp g hg₂ • f) = (TemperedDistribution.smulLeftCLM F g) (toTemperedDistribution f)

Coercion of the product of two Lp functions to a tempered distribution is equal to the left multiplication if the left factor is a function of temperate growth.

Derivatives

noncomputable def TemperedDistribution.derivCLM (F : Type u_4) [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 ℂ ℂ)

@[simp]

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

theorem TemperedDistribution.derivCLM_toTemperedDistributionCLM_eq (𝕜 : Type u_2) {F : Type u_4} [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)

@[implicit_reducible]

noncomputable instance TemperedDistribution.instLineDeriv {E : Type u_3} {F : Type u_4} [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.

@[simp]

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

instance TemperedDistribution.instLineDerivAdd {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℂ F] : LineDerivAdd E (TemperedDistribution E F) (TemperedDistribution E F)

instance TemperedDistribution.instLineDerivSMulComplex {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℂ F] : LineDerivSMul ℂ E (TemperedDistribution E F) (TemperedDistribution E F)

instance TemperedDistribution.instLineDerivSMulReal {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℂ F] : LineDerivSMul ℝ E (TemperedDistribution E F) (TemperedDistribution E F)

instance TemperedDistribution.instLineDerivLeftSMulReal {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℂ F] : LineDerivLeftSMul ℝ E (TemperedDistribution E F) (TemperedDistribution E F)

instance TemperedDistribution.instContinuousLineDeriv {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℂ F] : ContinuousLineDeriv E (TemperedDistribution E F) (TemperedDistribution E F)

theorem TemperedDistribution.lineDerivOpCLM_eq {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℂ F] (m : E) : LineDeriv.lineDerivOpCLM ℂ (TemperedDistribution E F) m = PointwiseConvergenceCLM.precomp F (-LineDeriv.lineDerivOpCLM ℂ (SchwartzMap E ℂ) m)

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

Laplacian

@[implicit_reducible]

noncomputable instance TemperedDistribution.instLaplacian {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [NormedSpace ℂ F] : Laplacian (TemperedDistribution E F) (TemperedDistribution E F)

Equations

• TemperedDistribution.instLaplacian = { laplacian := ⇑(LineDeriv.laplacianCLM ℝ E (TemperedDistribution E F)) }

@[simp]

theorem TemperedDistribution.laplacianCLM_apply {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [NormedSpace ℂ F] (f : TemperedDistribution E F) : (LineDeriv.laplacianCLM ℂ E (TemperedDistribution E F)) f = Laplacian.laplacian f

theorem TemperedDistribution.laplacian_eq_sum {ι : Type u_1} {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [NormedSpace ℂ F] [Fintype ι] (b : OrthonormalBasis ι ℝ E) (f : TemperedDistribution E F) : Laplacian.laplacian f = ∑ i : ι, LineDeriv.lineDerivOp (b i) (LineDeriv.lineDerivOp (b i) f)

@[simp]

theorem TemperedDistribution.laplacian_apply_apply {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [NormedSpace ℂ F] (f : TemperedDistribution E F) (u : SchwartzMap E ℂ) : (Laplacian.laplacian f) u = f (Laplacian.laplacian u)

@[simp]

theorem TemperedDistribution.laplacian_toTemperedDistributionCLM_eq {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [NormedSpace ℂ F] [MeasurableSpace E] [BorelSpace E] (f : SchwartzMap E F) : Laplacian.laplacian ((SchwartzMap.toTemperedDistributionCLM E F MeasureTheory.volume) f) = (SchwartzMap.toTemperedDistributionCLM E F MeasureTheory.volume) (Laplacian.laplacian f)

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

Fourier transform

@[implicit_reducible]

noncomputable instance TemperedDistribution.instFourierTransform {E : Type u_3} {F : Type u_4} [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 := ⇑(PointwiseConvergenceCLM.precomp F (FourierTransform.fourierCLM ℂ (SchwartzMap E ℂ))) }

instance TemperedDistribution.instFourierAdd {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [NormedSpace ℂ F] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] : FourierAdd (TemperedDistribution E F) (TemperedDistribution E F)

instance TemperedDistribution.instFourierSMul {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [NormedSpace ℂ F] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] : FourierSMul ℂ (TemperedDistribution E F) (TemperedDistribution E F)

instance TemperedDistribution.instContinuousFourier {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [NormedSpace ℂ F] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] : ContinuousFourier (TemperedDistribution E F) (TemperedDistribution E F)

@[simp]

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

@[deprecated FourierTransform.fourierCLM (since := "2026-01-06")]

def TemperedDistribution.fourierTransformCLM (R : Type u_2) (E : Type u_3) {F : Type u_4} [Semiring R] [AddCommMonoid E] [AddCommMonoid F] [Module R E] [Module R F] [FourierTransform E F] [FourierAdd E F] [FourierSMul R E F] [TopologicalSpace E] [TopologicalSpace F] [ContinuousFourier E F] : E →L[R] F

Alias of FourierTransform.fourierCLM.

Equations

• TemperedDistribution.fourierTransformCLM = FourierTransform.fourierCLM

@[deprecated FourierTransform.fourierCLM_apply (since := "2026-01-06")]

theorem TemperedDistribution.fourierTransformCLM_apply {R : Type u_2} {E : Type u_3} {F : Type u_4} [Semiring R] [AddCommMonoid E] [AddCommMonoid F] [Module R E] [Module R F] [FourierTransform E F] [FourierAdd E F] [FourierSMul R E F] [TopologicalSpace E] [TopologicalSpace F] [ContinuousFourier E F] (f : E) : (FourierTransform.fourierCLM R E) f = FourierTransform.fourier f

Alias of FourierTransform.fourierCLM_apply.

@[deprecated TemperedDistribution.fourier_apply (since := "2026-01-06")]

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

Alias of TemperedDistribution.fourier_apply.

@[implicit_reducible]

noncomputable instance TemperedDistribution.instFourierTransformInv {E : Type u_3} {F : Type u_4} [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 := ⇑(PointwiseConvergenceCLM.precomp F (FourierTransform.fourierInvCLM ℂ (SchwartzMap E ℂ))) }

instance TemperedDistribution.instFourierInvAdd {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [NormedSpace ℂ F] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] : FourierInvAdd (TemperedDistribution E F) (TemperedDistribution E F)

instance TemperedDistribution.instFourierInvSMul {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [NormedSpace ℂ F] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] : FourierInvSMul ℂ (TemperedDistribution E F) (TemperedDistribution E F)

instance TemperedDistribution.instContinuousFourierInv {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [NormedSpace ℂ F] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] : ContinuousFourierInv (TemperedDistribution E F) (TemperedDistribution E F)

@[simp]

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

@[deprecated FourierTransform.fourierInvCLM (since := "2026-01-06")]

def TemperedDistribution.fourierTransformInvCLM (R : Type u_2) (E : Type u_3) {F : Type u_4} [Semiring R] [AddCommMonoid E] [AddCommMonoid F] [Module R E] [Module R F] [FourierTransformInv E F] [FourierInvAdd E F] [FourierInvSMul R E F] [TopologicalSpace E] [TopologicalSpace F] [ContinuousFourierInv E F] : E →L[R] F

Alias of FourierTransform.fourierInvCLM.

Equations

• TemperedDistribution.fourierTransformInvCLM = FourierTransform.fourierInvCLM

@[deprecated FourierTransform.fourierInvCLM_apply (since := "2026-01-06")]

theorem TemperedDistribution.fourierTransformInvCLM_apply {R : Type u_2} {E : Type u_3} {F : Type u_4} [Semiring R] [AddCommMonoid E] [AddCommMonoid F] [Module R E] [Module R F] [FourierTransformInv E F] [FourierInvAdd E F] [FourierInvSMul R E F] [TopologicalSpace E] [TopologicalSpace F] [ContinuousFourierInv E F] (f : E) : (FourierTransform.fourierInvCLM R E) f = FourierTransformInv.fourierInv f

Alias of FourierTransform.fourierInvCLM_apply.

@[deprecated TemperedDistribution.fourierInv_apply (since := "2026-01-06")]

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

Alias of TemperedDistribution.fourierInv_apply.

instance TemperedDistribution.instFourierPair {E : Type u_3} {F : Type u_4} [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_3} {F : Type u_4} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [NormedSpace ℂ F] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] : FourierInvPair (TemperedDistribution E F) (TemperedDistribution E F)

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

@[deprecated TemperedDistribution.fourier_toTemperedDistributionCLM_eq (since := "2026-01-14")]

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

Alias of TemperedDistribution.fourier_toTemperedDistributionCLM_eq.

---

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

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

@[deprecated TemperedDistribution.fourierInv_toTemperedDistributionCLM_eq (since := "2026-01-14")]

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

Alias of TemperedDistribution.fourierInv_toTemperedDistributionCLM_eq.

---

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

theorem TemperedDistribution.lineDerivOp_fourier_eq {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [NormedSpace ℂ F] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (f : TemperedDistribution E F) (m : E) : LineDeriv.lineDerivOp m (FourierTransform.fourier f) = FourierTransform.fourier (-(2 * ↑Real.pi * Complex.I) • (smulLeftCLM F fun (x : E) => ↑(inner ℝ x m)) f)

theorem TemperedDistribution.fourier_lineDerivOp_eq {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [NormedSpace ℂ F] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (f : TemperedDistribution E F) (m : E) : FourierTransform.fourier (LineDeriv.lineDerivOp m f) = (2 * ↑Real.pi * Complex.I) • (smulLeftCLM F fun (x : E) => ↑(inner ℝ x m)) (FourierTransform.fourier f)

theorem TemperedDistribution.lineDerivOp_fourierInv_eq {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [NormedSpace ℂ F] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (f : TemperedDistribution E F) (m : E) : LineDeriv.lineDerivOp m (FourierTransformInv.fourierInv f) = FourierTransformInv.fourierInv ((2 * ↑Real.pi * Complex.I) • (smulLeftCLM F fun (x : E) => ↑(inner ℝ x m)) f)

theorem TemperedDistribution.fourierInv_lineDerivOp_eq {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [NormedSpace ℂ F] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (f : TemperedDistribution E F) (m : E) : FourierTransformInv.fourierInv (LineDeriv.lineDerivOp m f) = -(2 * ↑Real.pi * Complex.I) • (smulLeftCLM F fun (x : E) => ↑(inner ℝ x m)) (FourierTransformInv.fourierInv f)

noncomputable def TemperedDistribution.delta {E : Type u_3} [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.

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

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

Alias of TemperedDistribution.delta.

---

The Dirac delta distribution

Equations

• @SchwartzMap.delta = @TemperedDistribution.delta

@[simp]

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

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

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

Alias of TemperedDistribution.delta_apply.

@[simp]

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

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

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

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