theorem SchwartzRepresentation.hasTemperateGrowth_finset_prod {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {R : Type u_2} [NormedCommRing R] [NormedAlgebra ℝ R] {ι : Type u_3} {f : ι → E → R} {s : Finset ι} (hf : ∀ i ∈ s, Function.HasTemperateGrowth (f i)) : Function.HasTemperateGrowth fun (x : E) => ∏ i ∈ s, f i x

A finite product of functions of temperate growth (in the sense of Schwartz) is again of temperate growth, proved by induction on the finset using closure of HasTemperateGrowth under multiplication.

theorem SchwartzRepresentation.monomial_hasTemperateGrowth {n : ℕ} (α : Fin n → ℕ) : Function.HasTemperateGrowth (monomial α)

Every monomial x^α on ℝⁿ has temperate growth: it is the product of coordinate-power functions, each of which is of temperate growth.

theorem SchwartzRepresentation.sobolev_intermediate_form (n : ℕ) (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) : ∃ (M : ℕ) (v : (Fin n → ℕ) → ZeroAtInftyContinuousMap (EuclideanSpace ℝ (Fin n)) ℂ), ∀ (φ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ), u φ = ∑ γ ∈ multiIndicesBall n M, c0SchwartzPairing (v γ) (iterSchwartzDeriv γ φ)

Intermediate Sobolev-type representation of a tempered distribution: every u ∈ 𝓢'(ℝⁿ, ℂ) can be written as a finite sum of pairings of C₀ functions with iterated derivatives of the Schwartz test function, indexed over a ball of multi-indices. This is the form (10.10) used in the proof of Theorem 10.5 (Schwartz representation).

theorem SchwartzRepresentation.leibniz_rewrite (n M : ℕ) (v : (Fin n → ℕ) → ZeroAtInftyContinuousMap (EuclideanSpace ℝ (Fin n)) ℂ) : ∃ (m : ℕ) (f : (Fin n → ℕ) → (Fin n → ℕ) → ZeroAtInftyContinuousMap (EuclideanSpace ℝ (Fin n)) ℂ), ∀ (φ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ), ∑ γ ∈ multiIndicesBall n M, c0SchwartzPairing (v γ) (iterSchwartzDeriv γ φ) = ∑ α ∈ multiIndicesBall n m, ∑ β ∈ multiIndicesBall n m, c0SchwartzPairing (f α β) (iterSchwartzDeriv β ((SchwartzMap.smulLeftCLM ℂ (monomial α)) φ))

Leibniz-rule rewrite of the intermediate Sobolev representation: any expression of the form ∑ c0SchwartzPairing (v γ) (∂^γ φ) can be rewritten as a double sum over multi-indices (α, β) of pairings against ∂^β (x^α · φ).

theorem SchwartzRepresentation.schwartz_representation_improved (n : ℕ) (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) : ∃ (m : ℕ) (f : (Fin n → ℕ) → (Fin n → ℕ) → ZeroAtInftyContinuousMap (EuclideanSpace ℝ (Fin n)) ℂ), ∀ (φ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ), u φ = ∑ α ∈ multiIndicesBall n m, ∑ β ∈ multiIndicesBall n m, c0SchwartzPairing (f α β) (iterSchwartzDeriv β ((SchwartzMap.smulLeftCLM ℂ (monomial α)) φ))

Schwartz representation theorem (Theorem 10.5 of Melrose), improved form: every tempered distribution u ∈ 𝓢'(ℝⁿ, ℂ) is given by a finite sum over multi-indices (α, β) of pairings of C₀ functions f α β with ∂^β (x^α · φ).