theorem TemperedDistributions.continuous_of_seminorm_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (u : SchwartzMap E ℂ →ₗ[ℂ] ℂ) (hbound : ∃ (s : Finset (ℕ × ℕ)) (C : NNReal), (normSeminorm ℂ ℂ).comp u ≤ C • s.sup (schwartzSeminormFamily ℂ E ℂ)) : Continuous ⇑u

A linear functional on Schwartz space is continuous as soon as its norm seminorm is dominated by a finite sup of Schwartz seminorms times a constant.

theorem TemperedDistributions.seminorm_bound_of_continuous {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (u : SchwartzMap E ℂ →L[ℂ] ℂ) : ∃ (s : Finset (ℕ × ℕ)) (C : NNReal), (normSeminorm ℂ ℂ).comp ↑u ≤ C • s.sup (schwartzSeminormFamily ℂ E ℂ)

Conversely, every continuous linear functional on Schwartz space is dominated by a finite sup of Schwartz seminorms times a constant.

theorem TemperedDistributions.continuous_iff_seminorm_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (u : SchwartzMap E ℂ →ₗ[ℂ] ℂ) : Continuous ⇑u ↔ ∃ (s : Finset (ℕ × ℕ)) (C : NNReal), (normSeminorm ℂ ℂ).comp u ≤ C • s.sup (schwartzSeminormFamily ℂ E ℂ)

Continuity of a linear functional on Schwartz space is equivalent to a Schwartz-seminorm bound (Melrose Prop 7.3): this is the characterisation of tempered distributions.

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

Continuous embedding Lp(F, μ) → 𝓢'(E, F) sending an Lᵖ-function to the tempered distribution it represents.

noncomputable def TemperedDistributions.distribDerivCLM {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] (m : E) : TemperedDistribution E F →L[ℂ] TemperedDistribution E F

Distributional directional derivative in direction m: a continuous linear endomorphism of 𝓢'(E, F) given by u ↦ u ∘ (-∂_m).

@[simp]

theorem TemperedDistributions.distribDerivCLM_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] (m : E) (u : TemperedDistribution E F) (φ : SchwartzMap E ℂ) : ((distribDerivCLM m) u) φ = u (-LineDeriv.lineDerivOp m φ)

The definitional unfolding of distribDerivCLM: it pairs u with -(∂_m φ).

noncomputable def TemperedDistributions.distribMulCLM {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] (g : E → ℂ) : TemperedDistribution E F →L[ℂ] TemperedDistribution E F

Distributional multiplication by a (necessarily temperate) function g : E → ℂ, as a continuous linear endomorphism of 𝓢'(E, F).

@[simp]

theorem TemperedDistributions.distribMulCLM_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] (g : E → ℂ) (u : TemperedDistribution E F) (φ : SchwartzMap E ℂ) : ((distribMulCLM g) u) φ = u ((SchwartzMap.smulLeftCLM ℂ g) φ)

The definitional unfolding of distribMulCLM g: it pairs u with g · φ.

theorem TemperedDistributions.schwartz_iff_oneAddNorm_decay {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] {f : E → G} (hsmooth : ContDiff ℝ (↑⊤) f) : (∀ (k n : ℕ), ∃ (C : ℝ), ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C) ↔ ∀ (k n : ℕ), ∃ (C : ℝ), ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C

Equivalence of two formulations of Schwartz decay for a smooth function: the standard ‖x‖ᵏ polynomial growth control matches the variant using (1 + ‖x‖)ᵏ.

theorem TemperedDistributions.SchwartzMap.seminorm_derivCLM_le {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] (𝕜 : Type u_4) [RCLike 𝕜] [NormedSpace 𝕜 G] [SMulCommClass ℝ 𝕜 G] (k n : ℕ) (f : SchwartzMap ℝ G) : (SchwartzMap.seminorm 𝕜 k n) ((SchwartzMap.derivCLM 𝕜 G) f) ≤ (SchwartzMap.seminorm 𝕜 k (n + 1)) f

Differentiating in 𝓢(ℝ, G) shifts a Schwartz seminorm: the (k, n)-seminorm of f' is bounded by the (k, n + 1)-seminorm of f.

theorem TemperedDistributions.SchwartzMap.derivCLM_pow_eq_iterate {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] (𝕜 : Type u_4) [RCLike 𝕜] [NormedSpace 𝕜 G] (m : ℕ) (f : SchwartzMap ℝ G) : (SchwartzMap.derivCLM 𝕜 G ^ m) f = (⇑(SchwartzMap.derivCLM 𝕜 G))^[m] f

The m-th power of derivCLM equals its m-fold function iterate.

theorem TemperedDistributions.monomial_hasTemperateGrowth (α : ℕ) : Function.HasTemperateGrowth fun (x : ℝ) => x ^ α

Polynomial monomials x ↦ xᵅ are of temperate growth.

noncomputable def TemperedDistributions.SchwartzMap.polyMulDerivCLM {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] (α β : ℕ) : SchwartzMap ℝ G →L[ℝ] SchwartzMap ℝ G

Continuous linear operator on 𝓢(ℝ, G) given by f ↦ x^α · f^(β), i.e. the multiplication by the monomial xᵅ composed with β-fold differentiation.

theorem TemperedDistributions.seminorm_bound_of_continuous_linearMap {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] (𝕜 : Type u_4) [RCLike 𝕜] [NormedSpace 𝕜 G] [SMulCommClass ℝ 𝕜 G] (T : SchwartzMap E G →L[𝕜] SchwartzMap E G) : Seminorm.IsBounded (schwartzSeminormFamily 𝕜 E G) (schwartzSeminormFamily 𝕜 E G) ↑T

Every continuous linear endomorphism of 𝓢(E, G) is bounded with respect to the Schwartz seminorm family in the sense that each seminorm of T(f) is dominated by a finite sum of seminorms of f.

theorem TemperedDistributions.continuous_of_seminorm_bound_linearMap {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] (𝕜 : Type u_4) [RCLike 𝕜] [NormedSpace 𝕜 G] [SMulCommClass ℝ 𝕜 G] (T : SchwartzMap E G →ₗ[𝕜] SchwartzMap E G) (hbound : Seminorm.IsBounded (schwartzSeminormFamily 𝕜 E G) (schwartzSeminormFamily 𝕜 E G) T) : Continuous ⇑T

Conversely, a linear endomorphism of 𝓢(E, G) that is bounded with respect to the Schwartz seminorm family is automatically continuous.

theorem TemperedDistributions.dsupport_schwartz_subset_tsupport {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] [FiniteDimensional ℝ E] [MeasureTheory.MeasureSpace E] [BorelSpace E] [SecondCountableTopology E] [MeasureTheory.volume.IsAddHaarMeasure] (ψ : SchwartzMap E F) : Distribution.dsupport ⇑((SchwartzMap.toTemperedDistributionCLM E F MeasureTheory.volume) ψ) ⊆ tsupport ⇑ψ

The distributional support of the tempered distribution attached to a Schwartz function ψ is contained in the closure of the support of ψ.

theorem TemperedDistributions.support_subset_dsupport_schwartz {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] [FiniteDimensional ℝ E] [MeasureTheory.MeasureSpace E] [BorelSpace E] [SecondCountableTopology E] [MeasureTheory.volume.IsAddHaarMeasure] [CompleteSpace F] (ψ : SchwartzMap E F) : Function.support ⇑ψ ⊆ Distribution.dsupport ⇑((SchwartzMap.toTemperedDistributionCLM E F MeasureTheory.volume) ψ)

The support of a Schwartz function ψ is contained in the distributional support of the attached tempered distribution.

theorem TemperedDistributions.dsupport_schwartz_eq_tsupport {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] [FiniteDimensional ℝ E] [MeasureTheory.MeasureSpace E] [BorelSpace E] [SecondCountableTopology E] [MeasureTheory.volume.IsAddHaarMeasure] [CompleteSpace F] (ψ : SchwartzMap E F) : Distribution.dsupport ⇑((SchwartzMap.toTemperedDistributionCLM E F MeasureTheory.volume) ψ) = tsupport ⇑ψ

The distributional support of (the tempered distribution attached to) a Schwartz function coincides with its topological support.

theorem TemperedDistributions.dsupport_closed_and_eq_tsupport {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] [FiniteDimensional ℝ E] [MeasureTheory.MeasureSpace E] [BorelSpace E] [SecondCountableTopology E] [MeasureTheory.volume.IsAddHaarMeasure] [CompleteSpace F] (u : TemperedDistribution E F) (ψ : SchwartzMap E F) : IsClosed (Distribution.dsupport ⇑u) ∧ Distribution.dsupport ⇑((SchwartzMap.toTemperedDistributionCLM E F MeasureTheory.volume) ψ) = tsupport ⇑ψ

Joint statement: the distributional support of any tempered distribution is closed, and on Schwartz functions the distributional support coincides with the topological support.