Chapter 10: Schwartz Representation and Polynomial Weight Derivatives

This file formalizes Theorem 10.5 (Schwartz representation theorem for tempered distributions) and Lemma 10.6 (polynomial weight derivative identity) from the appendix on tempered distribution theory.

Both results are deep structural facts about tempered distributions. Their proofs are not given in the text.

Main results

• theorem_10_5_schwartz_representation — Theorem 10.5: Any tempered distribution on ℝⁿ is a finite sum of terms x^α D^β u_{αβ} where u_{αβ} ∈ C₀(ℝⁿ).
• lemma_10_6_polynomial_weight_derivative — Lemma 10.6: Identity expressing ⟨x⟩^k D^γ v as a sum of derivatives of polynomial-weighted terms.

References

These results are standard in the theory of tempered distributions; see e.g. Hörmander, The Analysis of Linear Partial Differential Operators I, Chapter 7.

Multi-index infrastructure

@[reducible, inline]

abbrev MultiIndex (n : ℕ) : Type

A multi-index of dimension n is a function Fin n → ℕ, representing the exponents of a monomial x^α or the orders of iterated partial derivatives D^α.

def MultiIndex.order {n : ℕ} (α : MultiIndex n) : ℕ

The total order (degree) of a multi-index: |α| = Σᵢ αᵢ.

def MultiIndex.le {n : ℕ} (α γ : MultiIndex n) : Prop

Componentwise comparison of multi-indices: α ≤ γ iff αᵢ ≤ γᵢ for all i.

@[implicit_reducible]

instance MultiIndex.decidableLe {n : ℕ} (α γ : MultiIndex n) : Decidable (α.le γ)

def MultiIndex.sub {n : ℕ} (γ α : MultiIndex n) : MultiIndex n

Componentwise subtraction of multi-indices (using natural number subtraction).

def MultiIndex.finsetLe {n : ℕ} (γ : MultiIndex n) : Finset (MultiIndex n)

The set of multi-indices α with α ≤ γ (componentwise), as a Finset.

Distributional operations on ℝⁿ

noncomputable def iteratedSingleDerivTD {n : ℕ} (m : EuclideanSpace ℝ (Fin n)) (k : ℕ) (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ

Apply the directional derivative operator ∂_m to a tempered distribution k times.

noncomputable def multiDerivTD {n : ℕ} (β : MultiIndex n) (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ

The multi-index distributional derivative D^β u = ∂₁^{β₁} ∘ ⋯ ∘ ∂ₙ^{βₙ} u, where ∂ᵢ denotes the distributional partial derivative in the i-th coordinate direction (the direction of the standard basis vector eᵢ).

def monomialFun {n : ℕ} (α : MultiIndex n) : EuclideanSpace ℝ (Fin n) → ℂ

The monomial function x^α = ∏ᵢ xᵢ^{αᵢ} as a ℂ-valued function on ℝⁿ.

noncomputable def monomialMulTD {n : ℕ} (α : MultiIndex n) (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ

Multiplication of a tempered distribution by the monomial x^α.

noncomputable def japaneseBracket {n : ℕ} (x : EuclideanSpace ℝ (Fin n)) : ℝ

The Japanese bracket ⟨x⟩ = √(1 + ‖x‖²), which satisfies ⟨x⟩ ≥ 1 for all x.

noncomputable def japaneseBracketZPow {n : ℕ} (k : ℤ) : EuclideanSpace ℝ (Fin n) → ℂ

The Japanese bracket raised to integer power k, as a ℂ-valued function: ⟨x⟩^k = (√(1 + ‖x‖²))^k.

noncomputable def japaneseBracketMulTD {n : ℕ} (k : ℤ) (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ

Multiplication of a tempered distribution by ⟨x⟩^k.

noncomputable def evalMvPoly {n : ℕ} (P : MvPolynomial (Fin n) ℂ) (x : EuclideanSpace ℝ (Fin n)) : ℂ

Evaluate a multivariate polynomial P ∈ ℂ[x₁, …, xₙ] at a point of ℝⁿ, viewing the real coordinates as complex numbers.

C₀ representability

def TemperedDistribution.IsFromC0 {n : ℕ} (v : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) : Prop

A tempered distribution v is representable by a continuous function vanishing at infinity if there exists g ∈ C₀(ℝⁿ, ℂ) such that v(φ) = ∫ g(x) · φ(x) dx for all Schwartz test functions φ.

Theorem 10.5: Schwartz Representation Theorem (Goal 73)

Theorem 10.5 (Schwartz representation) — every tempered distribution is a finite sum of derivatives of continuous functions of polynomial growth. Any tempered distribution u on ℝⁿ can be written as u = Σ_{(α,β) ∈ S} x^α · D^β u_{αβ} where each u_{αβ} is a tempered distribution arising from a continuous function vanishing at infinity (u_{αβ} ∈ C₀(ℝⁿ)). The proof is not given in the text.

theorem theorem_10_5_schwartz_representation (n : ℕ) (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) : ∃ (S : Finset (MultiIndex n × MultiIndex n)) (v : MultiIndex n × MultiIndex n → TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ), (∀ p ∈ S, (v p).IsFromC0) ∧ u = ∑ p ∈ S, monomialMulTD p.1 (multiDerivTD p.2 (v p))

Goal 73: Theorem 10.5 (Schwartz representation) — every tempered distribution on ℝⁿ can be written as a finite sum u = Σ_{(α,β) ∈ S} x^α · D^β u_{αβ} where each u_{αβ} is a tempered distribution arising from a continuous function vanishing at infinity.

The proof is not given in the text. This is a deep structural result in the theory of tempered distributions; see e.g. Hörmander, The Analysis of Linear Partial Differential Operators I, Chapter 7.

Lemma 10.6: Polynomial Weight Derivative Identity (Goal 74)

Lemma 10.6 — for any γ ∈ ℕ₀ⁿ, there are polynomials p_{α,γ}(x) of degrees at most |γ - α| such that ⟨x⟩^k D^γ v = Σ_{α≤γ} D^{γ-α}(p_{α,γ} ⟨x⟩^{k-2|γ-α|} v). This identity relates weighted derivatives to sums of derivatives of weighted terms. The proof is not given in the text.

theorem lemma_10_6_polynomial_weight_derivative {n : ℕ} (γ : MultiIndex n) (k : ℤ) : ∃ (P : MultiIndex n → MvPolynomial (Fin n) ℂ), (∀ (α : MultiIndex n), α.le γ → (P α).totalDegree ≤ (γ.sub α).order) ∧ ∀ (v : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ), japaneseBracketMulTD k (multiDerivTD γ v) = ∑ α ∈ γ.finsetLe, multiDerivTD (γ.sub α) ((TemperedDistribution.smulLeftCLM ℂ fun (x : EuclideanSpace ℝ (Fin n)) => evalMvPoly (P α) x * japaneseBracketZPow (k - 2 * ↑(γ.sub α).order) x) v)

Goal 74: Lemma 10.6 — for any multi-index γ and integer k, there exist polynomials P α of total degree at most |γ - α| such that ⟨x⟩^k D^γ v equals the sum over α ≤ γ of D^{γ-α}(P_α · ⟨x⟩^{k-2|γ-α|} · v).

The proof is not given in the text. This is a standard identity in the theory of tempered distributions; see e.g. Hörmander, The Analysis of Linear Partial Differential Operators I, Chapter 7.