Chapter 11: Advanced Results — Convolution, Sobolev Spaces, and Laplace Equation

This file formalizes Goals 80–91 from Chapter 11 on distribution convolution, Sobolev spaces, and the Laplace equation. These are deep PDE/functional analysis results from an appendix chapter; the book does not provide full proofs for any of these results, so they are stated as axioms.

Main definitions and results

• MemSobolevSpace: Definition 11.8 — Membership in the Sobolev space H^s(ℝⁿ)
• fractionalLaplacian: Definition 11.11 — The fractional Laplacian (-Δ)^{s/2}
• theorem_11_6_hormander: Theorem 11.6 (a) — u * φ is C^∞ with temperate growth
• DistribSupport: Distributional support of a tempered distribution
• theorem_11_6_support: Theorem 11.6 (b) — supp(u * φ) ⊆ supp(u) + supp(φ)
• iterLineDerivSchwartz, iterMultiDerivSchwartz: Iterated derivatives for Schwartz functions
• theorem_11_6_deriv_commutes: Theorem 11.6 (c) — D^α(u * φ) = D^α u * φ = u * D^α φ
• lemma_11_7_approx_identity: Lemma 11.7 — Approximate identity convergence
• theorem_11_9_sobolev_characterization: Theorem 11.9 — H^k via multi-index derivatives
• theorem_11_9_hypoelliptic_singsupp: Theorem 11.9 — sing supp(u) = sing supp(P(D)u) for hypoelliptic P(D)
• lemma_11_10_singsupp_inclusion: Lemma 11.10 — sing supp(P(D)u) ⊆ sing supp(u)
• lemma_11_10_sobolev_embedding: Lemma 11.10 — Sobolev embedding H^s ↪ C^k
• theorem_11_12_bessel_potential: Theorem 11.12 — Bessel potential spaces
• lemma_11_13_sobolev_multiplication: Lemma 11.13 — Sobolev multiplication
• lemma_11_14_interpolation: Lemma 11.14 — Interpolation in Sobolev spaces
• lemma_11_14_deriv_reciprocal_bound: Lemma 11.14 — Derivative bound for 1/P(ξ)
• HasCompactDistribSupport: Compact support for tempered distributions
• distribConvolution: Convolution of compactly supported distribution with any distribution
• prop_11_15_singsupp_convolution: Proposition 11.15 — sing supp(u * f) ⊆ sing supp(u) + sing supp(f)
• prop_11_15_trace: Proposition 11.15 — Trace theorem
• prop_11_16_extension: Proposition 11.16 — Extension theorem
• heatOp: The heat operator (∂_t + Δ_x) on S'(ℝⁿ⁺¹)
• HasSupportInFutureHalfSpace: Support condition supp(u) ⊆ {t ≥ -T}
• prop_11_16_heat_equation: Proposition 11.16 — Heat equation existence/uniqueness
• theorem_11_17_laplace_equation: Theorem 11.17 — Δu = f existence/uniqueness
• theorem_11_12_elliptic_hypoelliptic: Theorem 11.12 — Every elliptic P(D) is hypoelliptic

@[reducible, inline]

abbrev Chapter11.Rn (n : ℕ) : Type

Standard abbreviation for ℝⁿ = EuclideanSpace ℝ (Fin n).

Helper definitions

noncomputable def Chapter11.evalPolyAtRn (n : ℕ) (P : MvPolynomial (Fin n) ℂ) (ξ : Rn n) : ℂ

Evaluate a multivariate polynomial P ∈ ℂ[ξ₁,…,ξₙ] at a point ξ ∈ ℝⁿ, embedding each real coordinate into ℂ. This is the composition of MvPolynomial.aeval with the coordinate projection Rn n → Fin n → ℝ → ℂ.

def Chapter11.embedHyperplane (n : ℕ) (x : Rn n) : Rn (n + 1)

Embedding of ℝⁿ into ℝⁿ⁺¹ as the hyperplane {xₙ₊₁ = 0}. This maps (x₁, ..., xₙ) to (x₁, ..., xₙ, 0).

def Chapter11.liftPoint (n : ℕ) (ξ' : Rn n) (t : ℝ) : Rn (n + 1)

Lift a point ξ' ∈ ℝⁿ and a coordinate t ∈ ℝ to (ξ', t) ∈ ℝⁿ⁺¹.

noncomputable def Chapter11.fourierTrace (n : ℕ) (f : Rn (n + 1) → ℂ) : Rn n → ℂ

The Fourier-side trace operator: given a function f on ℝⁿ⁺¹, integrate out the last variable to get a function on ℝⁿ. On the Fourier side, this corresponds to restriction to the hyperplane {xₙ₊₁ = 0}.

noncomputable def Chapter11.stdBasisVec (n : ℕ) (i : Fin n) : Rn n

Standard basis vector eᵢ in ℝⁿ.

def Chapter11.iterLineDeriv {n : ℕ} (v : Rn n) : ℕ → TemperedDistribution (Rn n) ℂ → TemperedDistribution (Rn n) ℂ

Iterated distributional line derivative ∂ᵥᵏ u.

noncomputable def Chapter11.iterMultiDeriv (n : ℕ) (α : Fin n → ℕ) (u : TemperedDistribution (Rn n) ℂ) : TemperedDistribution (Rn n) ℂ

Iterated multi-index distributional derivative D^α u where α : Fin n → ℕ is a multi-index. Applies α i derivatives in the direction eᵢ for each coordinate i, composing all of them. Since distributional partial derivatives commute, the order of composition does not matter.

def Chapter11.IsL2Represented {n : ℕ} (u : TemperedDistribution (Rn n) ℂ) : Prop

A tempered distribution is represented by an L² function, i.e., there exists f ∈ L² such that u(φ) = ∫ f · φ for all Schwartz φ.

Theorem 11.6: Hörmander convolution theorem (Goal 80)

For u ∈ S'(ℝⁿ) and φ ∈ S(ℝⁿ), the convolution u * φ is a smooth function with at most polynomial growth. Moreover, (u * φ)(x) = u(τ_x φ̌).

theorem Chapter11.theorem_11_6_hormander (n : ℕ) (u : TemperedDistribution (Rn n) ℂ) (φ : SchwartzMap (Rn n) ℂ) : ∃ (f : Rn n → ℂ), ContDiff ℝ ⊤ f ∧ Function.HasTemperateGrowth f ∧ ∀ (ψ : SchwartzMap (Rn n) ℂ), ∫ (x : Rn n), f x • ((SchwartzMap.fourierTransformCLM ℂ) ψ) x = ((TemperedDistribution.smulLeftCLM ℂ ⇑((SchwartzMap.fourierTransformCLM ℂ) φ)) (FourierTransform.fourier u)) ψ

The proof is not given in the textbook, so we axiomatize it.

Theorem 11.6 (b): Support property

If φ ∈ S(ℝⁿ) has compact support and f is the smooth representative of u * φ, then supp(f) ⊆ supp(u) + supp(φ), where supp(u) is the distributional support and + denotes the Minkowski sum. The proof is not given in the textbook.

def Chapter11.DistribSupport {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasureTheory.MeasureSpace E] [BorelSpace E] [SecondCountableTopology E] [FiniteDimensional ℝ E] [MeasureTheory.volume.HasTemperateGrowth] (u : TemperedDistribution E ℂ) : Set E

The distributional support of a tempered distribution u ∈ S'(E, ℂ). A point x belongs to DistribSupport u if u does not vanish in any neighborhood of x. Formally, x ∈ DistribSupport u iff for every smooth compactly supported function φ with φ(x) ≠ 0, it is not the case that u vanishes on all test functions supported within the support of φ.

theorem Chapter11.theorem_11_6_support (n : ℕ) (u : TemperedDistribution (Rn n) ℂ) (φ : SchwartzMap (Rn n) ℂ) (hφ : HasCompactSupport ⇑φ) (f : Rn n → ℂ) (hf_smooth : ContDiff ℝ ⊤ f) (hf_repr : ∀ (ψ : SchwartzMap (Rn n) ℂ), ∫ (x : Rn n), f x • ((SchwartzMap.fourierTransformCLM ℂ) ψ) x = ((TemperedDistribution.smulLeftCLM ℂ ⇑((SchwartzMap.fourierTransformCLM ℂ) φ)) (FourierTransform.fourier u)) ψ) : Function.support f ⊆ DistribSupport u + Function.support ⇑φ

Theorem 11.6 (b) (Support of convolution with Schwartz function): If u ∈ S'(ℝⁿ) and φ ∈ S(ℝⁿ) has compact support, and f is the smooth representative of u * φ (as produced by Theorem 11.6 (a)), then supp(f) ⊆ DistribSupport(u) + supp(φ) where + is the Minkowski sum. The proof is not given in the textbook.

Theorem 11.6 (c): Derivative commutativity

For any multi-index α, D^α(u * φ) = (D^α u) * φ = u * (D^α φ). This expresses the fact that differentiation of the convolution u * φ can be applied to either factor. On the Fourier side this follows from the multiplicative structure of the Fourier symbol.

The proof is not given in the textbook.

def Chapter11.iterLineDerivSchwartz {n : ℕ} (v : Rn n) : ℕ → SchwartzMap (Rn n) ℂ → SchwartzMap (Rn n) ℂ

Iterated line derivative for Schwartz functions (analogous to iterLineDeriv for tempered distributions).

noncomputable def Chapter11.iterMultiDerivSchwartz (n : ℕ) (α : Fin n → ℕ) (φ : SchwartzMap (Rn n) ℂ) : SchwartzMap (Rn n) ℂ

Iterated multi-index derivative for Schwartz functions D^α φ where α : Fin n → ℕ is a multi-index. Applies α i derivatives in the direction eᵢ for each coordinate i, composing all of them.

theorem Chapter11.theorem_11_6_deriv_commutes (n : ℕ) (u : TemperedDistribution (Rn n) ℂ) (φ : SchwartzMap (Rn n) ℂ) (α : Fin n → ℕ) (ψ : SchwartzMap (Rn n) ℂ) : ((TemperedDistribution.smulLeftCLM ℂ ⇑((SchwartzMap.fourierTransformCLM ℂ) φ)) (FourierTransform.fourier (iterMultiDeriv n α u))) ψ = ((TemperedDistribution.smulLeftCLM ℂ ⇑((SchwartzMap.fourierTransformCLM ℂ) (iterMultiDerivSchwartz n α φ))) (FourierTransform.fourier u)) ψ

Theorem 11.6 (c) (Derivative commutativity for convolution): For u ∈ S'(ℝⁿ), φ ∈ S(ℝⁿ), and any multi-index α, D^α(u * φ) = (D^α u) * φ = u * (D^α φ).

This is stated as the equality of the Fourier-side convolution products: the convolution of D^α u with φ produces the same tempered distribution as the convolution of u with D^α φ. The proof is not given in the textbook.

Lemma 11.7: Approximate identity (Goal 81)

If φ ∈ S(ℝⁿ) with ∫ φ = 1 and φ_ε(x) = ε⁻ⁿ φ(x/ε), then φ_ε → δ in S'(ℝⁿ) as ε → 0⁺.

theorem Chapter11.lemma_11_7_approx_identity (n : ℕ) (φ : SchwartzMap (Rn n) ℂ) (hint : ∫ (x : Rn n), φ x = 1) (ψ : SchwartzMap (Rn n) ℂ) : Filter.Tendsto (fun (ε : ℝ) => ∫ (x : Rn n), ε⁻¹ ^ n • φ (ε⁻¹ • x) * ψ x) (nhdsWithin 0 (Set.Ioi 0)) (nhds (ψ 0))

The proof is not given in the textbook, so we axiomatize it.

Definition 11.8: Sobolev space H^s (Goal 82)

def Chapter11.MemSobolevSpace (n : ℕ) (s : ℝ) (u : TemperedDistribution (Rn n) ℂ) : Prop

Goal 82

@[reducible, inline]

abbrev Chapter11.def_11_8_sobolev (n : ℕ) (s : ℝ) (u : TemperedDistribution (Rn n) ℂ) : Prop

Alias for the evaluator.

Theorem 11.9: H^k characterization via multi-index derivatives (Goal 83)

For a non-negative integer k, u ∈ H^k(ℝⁿ) if and only if all distributional partial derivatives D^α u with |α| ≤ k are in L²(ℝⁿ). This is a non-trivial equivalence between the Fourier-weight characterization and the derivative characterization.

theorem Chapter11.theorem_11_9_sobolev_characterization (n k : ℕ) (u : TemperedDistribution (Rn n) ℂ) : MemSobolevSpace n (↑k) u ↔ ∀ (α : Fin n → ℕ), ∑ i : Fin n, α i ≤ k → IsL2Represented (iterMultiDeriv n α u)

The proof is not given in the textbook, so we axiomatize it.

Theorem 11.9: Hypoelliptic operators preserve singular support

If P(D) is hypoelliptic then sing supp(u) = sing supp(P(D)u) for all u ∈ S'(ℝⁿ). The proof is not given in the textbook.

theorem Chapter11.theorem_11_9_hypoelliptic_singsupp {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasureTheory.MeasureSpace E] [BorelSpace E] [SecondCountableTopology E] [FiniteDimensional ℝ E] [MeasureTheory.volume.HasTemperateGrowth] (P : TemperedDistribution E ℂ →L[ℂ] TemperedDistribution E ℂ) (hP : IsHypoelliptic E P) (u : TemperedDistribution E ℂ) : SingularSupport E u = SingularSupport E (P u)

Theorem 11.9 (Hypoelliptic singular support equality): If P(D) is hypoelliptic (i.e., it admits a parametrix whose singular support is contained in {0}), then for every tempered distribution u ∈ S'(E, ℂ), sing supp(u) = sing supp(P(D)u).

Intuitively, a hypoelliptic operator cannot create or destroy singularities: the inclusion sing supp(P(D)u) ⊆ sing supp(u) holds for any constant-coefficient operator, and the reverse inclusion is the content of hypoellipticity — if P(D)u is smooth near a point, then u must also be smooth near that point.

The proof is not given in the textbook, so we axiomatize it.

Lemma 11.10: Singular support inclusion for P(D)

If u ∈ S'(ℝⁿ) then for any constant-coefficient differential operator P(D), sing supp(P(D)u) ⊆ sing supp(u). The proof is not given in the textbook.

theorem Chapter11.lemma_11_10_singsupp_inclusion {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasureTheory.MeasureSpace E] [BorelSpace E] [SecondCountableTopology E] [FiniteDimensional ℝ E] [MeasureTheory.volume.HasTemperateGrowth] (P : TemperedDistribution E ℂ →L[ℂ] TemperedDistribution E ℂ) (u : TemperedDistribution E ℂ) : SingularSupport E (P u) ⊆ SingularSupport E u

Lemma 11.10 (Singular support inclusion for P(D)): For any constant-coefficient differential operator P(D) modeled as a continuous linear endomorphism of S'(E, ℂ) and any tempered distribution u ∈ S'(E, ℂ), we have sing supp(P(D)u) ⊆ sing supp(u).

Intuitively, applying a differential operator with constant coefficients cannot create new singularities: the only points where P(D)u can fail to be smooth are points where u itself already fails to be smooth.

The proof is not given in the textbook, so we axiomatize it.

Lemma 11.10: Sobolev embedding (Goal 84)

theorem Chapter11.lemma_11_10_sobolev_embedding (n : ℕ) (s : ℝ) (k : ℕ) (hs : s > ↑n / 2 + ↑k) (u : TemperedDistribution (Rn n) ℂ) (hu : MemSobolevSpace n s u) : ∃ (f : Rn n → ℂ), ContDiff ℝ (↑k) f ∧ ∀ (φ : SchwartzMap (Rn n) ℂ), u φ = ∫ (x : Rn n), f x • φ x

The proof is not given in the textbook, so we axiomatize it.

Definition 11.11: Fractional Laplacian (Goal 85)

noncomputable def Chapter11.fractionalLaplacian (n : ℕ) (s : ℝ) : TemperedDistribution (Rn n) ℂ →L[ℂ] TemperedDistribution (Rn n) ℂ

Goal 85

@[reducible, inline]

noncomputable abbrev Chapter11.def_11_11_fractional_laplacian (n : ℕ) (s : ℝ) : TemperedDistribution (Rn n) ℂ →L[ℂ] TemperedDistribution (Rn n) ℂ

Alias for the evaluator.

Theorem 11.12: Bessel potential spaces (Goal 86)

theorem Chapter11.theorem_11_12_bessel_potential (n : ℕ) (s : ℝ) (u : TemperedDistribution (Rn n) ℂ) : MemSobolevSpace n s u ↔ ∃ (f : Rn n → ℂ), MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume ∧ (∀ (φ : SchwartzMap (Rn n) ℂ), ((TemperedDistribution.fourierMultiplierCLM ℂ fun (ξ : Rn n) => ↑((1 + 4 * Real.pi ^ 2 * ‖ξ‖ ^ 2) ^ (s / 2))) u) φ = ∫ (x : Rn n), f x • φ x) ∧ MeasureTheory.Integrable (fun (x : Rn n) => ‖f x‖ ^ 2) MeasureTheory.volume

The proof is not given in the textbook, so we axiomatize it.

Lemma 11.13: Sobolev multiplication (Goal 87)

theorem Chapter11.lemma_11_13_sobolev_multiplication (n : ℕ) (s : ℝ) (hs : s > ↑n / 2) (f g : Rn n → ℂ) (hf : MeasureTheory.Integrable (fun (ξ : Rn n) => (1 + ‖ξ‖ ^ 2) ^ s * ‖f ξ‖ ^ 2) MeasureTheory.volume) (hg : MeasureTheory.Integrable (fun (ξ : Rn n) => (1 + ‖ξ‖ ^ 2) ^ s * ‖g ξ‖ ^ 2) MeasureTheory.volume) : MeasureTheory.Integrable (fun (ξ : Rn n) => (1 + ‖ξ‖ ^ 2) ^ s * ‖(f * g) ξ‖ ^ 2) MeasureTheory.volume

The proof is not given in the textbook, so we axiomatize it.

Lemma 11.14: Interpolation in Sobolev spaces (Goal 88)

theorem Chapter11.lemma_11_14_interpolation (n : ℕ) (s₀ s₁ θ : ℝ) (hθ₀ : 0 ≤ θ) (hθ₁ : θ ≤ 1) (u : TemperedDistribution (Rn n) ℂ) (hu₀ : MemSobolevSpace n s₀ u) (hu₁ : MemSobolevSpace n s₁ u) : MemSobolevSpace n ((1 - θ) * s₀ + θ * s₁) u

The proof is not given in the textbook, so we axiomatize it.

Lemma 11.14: Derivative bound for reciprocal of a polynomial

Let P(ξ) be a polynomial of degree m satisfying |P(ξ)| ≥ C|ξ|^m in |ξ| > 1/C for some C > 0. Then |D^α (1/P(ξ))| ≤ C_α |ξ|^{-m-|α|} in |ξ| > 1/C. The proof is not given in the textbook.

theorem Chapter11.lemma_11_14_deriv_reciprocal_bound {n : ℕ} (P : MvPolynomial (Fin n) ℂ) (m : ℕ) (C : ℝ) (hC : 0 < C) (hdeg : P.totalDegree ≤ m) (hlow : ∀ (ξ : Rn n), ‖ξ‖ > 1 / C → ‖evalPolyAtRn n P ξ‖ ≥ C * ‖ξ‖ ^ m) (k : ℕ) : ∃ (C_k : ℝ), 0 < C_k ∧ ∀ (ξ : Rn n), ‖ξ‖ > 1 / C → ‖iteratedFDeriv ℝ k (fun (ξ : Rn n) => (evalPolyAtRn n P ξ)⁻¹) ξ‖ ≤ C_k * ‖ξ‖⁻¹ ^ (m + k)

Lemma 11.14 (Derivative bound for reciprocal of a polynomial): Let P(ξ) be a polynomial of degree at most m in n variables over ℂ, satisfying ‖P(ξ)‖ ≥ C · ‖ξ‖^m for all ξ ∈ ℝⁿ with ‖ξ‖ > 1/C (for some constant C > 0). Then for each derivative order k ∈ ℕ, there exists a constant C_k > 0 such that ‖(d/dξ)^k (1/P(ξ))‖ ≤ C_k · ‖ξ‖^{-(m+k)} for all ξ with ‖ξ‖ > 1/C.

Here (d/dξ)^k denotes the k-th iterated Fréchet derivative (iteratedFDeriv ℝ k), which subsumes all multi-index partial derivatives D^α with |α| = k. The proof is not given in the textbook (it is a standard result in the theory of elliptic differential operators), so we axiomatize it.

Proposition 11.15: Singular support of convolution

If u ∈ S'(ℝⁿ) has compact support and f ∈ S'(ℝⁿ), then sing supp(u * f) ⊂ sing supp(u) + sing supp(f).

We first need to formalize compact support for tempered distributions and the convolution of a compactly supported distribution with an arbitrary one. Since the proof is not given in the textbook, we axiomatize these.

def Chapter11.HasCompactDistribSupport {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (u : TemperedDistribution E ℂ) : Prop

A tempered distribution u ∈ S'(E, ℂ) has compact support if there exists a compact set K ⊆ E such that u(φ) = 0 for every Schwartz function φ that vanishes on K. Equivalently, u is supported in K in the distributional sense.

noncomputable def Chapter11.distribConvolution {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasureTheory.MeasureSpace E] [BorelSpace E] [SecondCountableTopology E] [FiniteDimensional ℝ E] [MeasureTheory.volume.HasTemperateGrowth] (u f : TemperedDistribution E ℂ) (hu : HasCompactDistribSupport u) : TemperedDistribution E ℂ

Convolution of a compactly supported tempered distribution with a tempered distribution. When u ∈ S'(E, ℂ) has compact support, the convolution u * f is a well-defined tempered distribution for any f ∈ S'(E, ℂ). Since the construction of this convolution is not provided in the textbook and is not available in Mathlib, we axiomatize its existence.

theorem Chapter11.prop_11_15_singsupp_convolution {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasureTheory.MeasureSpace E] [BorelSpace E] [SecondCountableTopology E] [FiniteDimensional ℝ E] [MeasureTheory.volume.HasTemperateGrowth] (u f : TemperedDistribution E ℂ) (hu : HasCompactDistribSupport u) : SingularSupport E (distribConvolution u f hu) ⊆ SingularSupport E u + SingularSupport E f

Proposition 11.15 (Singular support of convolution): If u ∈ S'(E, ℂ) has compact support and f ∈ S'(E, ℂ), then sing supp(u * f) ⊆ sing supp(u) + sing supp(f) where + denotes the Minkowski sum of sets. The proof is not given in the textbook, so we axiomatize it.

Proposition 11.15: Trace theorem (Goal 89)

The trace map is expressed on the Fourier side: the Fourier-side representative of the trace v is obtained by integrating the Fourier-side representative of u over the last variable, i.e., v̂(ξ') = ∫ û(ξ', t) dt. This formulation avoids the null-set issues that arise from pointwise restriction of arbitrary representatives to a hyperplane.

theorem Chapter11.prop_11_15_trace (n : ℕ) (s : ℝ) (hs : s > 1 / 2) (u : TemperedDistribution (Rn (n + 1)) ℂ) (hu : MemSobolevSpace (n + 1) s u) : ∃ (v : TemperedDistribution (Rn n) ℂ), MemSobolevSpace n (s - 1 / 2) v ∧ ∀ (f : Rn (n + 1) → ℂ), MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume → (∀ (φ : SchwartzMap (Rn (n + 1)) ℂ), (FourierTransform.fourier u) φ = ∫ (x : Rn (n + 1)), f x • φ x) → ∀ (ψ : SchwartzMap (Rn n) ℂ), (FourierTransform.fourier v) ψ = ∫ (ξ' : Rn n), fourierTrace n f ξ' • ψ ξ'

The proof is not given in the textbook, so we axiomatize it.

Proposition 11.16: Extension theorem (Goal 90)

The extension operator is a right inverse of the trace: the Fourier-side trace of the extension recovers the original distribution.

theorem Chapter11.prop_11_16_extension (n : ℕ) (s : ℝ) (v : TemperedDistribution (Rn n) ℂ) (hv : MemSobolevSpace n s v) : ∃ (u : TemperedDistribution (Rn (n + 1)) ℂ), MemSobolevSpace (n + 1) (s + 1 / 2) u ∧ ∀ (f : Rn (n + 1) → ℂ), MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume → (∀ (φ : SchwartzMap (Rn (n + 1)) ℂ), (FourierTransform.fourier u) φ = ∫ (x : Rn (n + 1)), f x • φ x) → ∀ (ψ : SchwartzMap (Rn n) ℂ), (FourierTransform.fourier v) ψ = ∫ (ξ' : Rn n), fourierTrace n f ξ' • ψ ξ'

The proof is not given in the textbook, so we axiomatize it.

Proposition 11.16: Heat equation existence/uniqueness

If f ∈ S'(ℝⁿ⁺¹) has compact support, then there exists a unique u ∈ S'(ℝⁿ⁺¹) with supp(u) ⊂ {t ≥ -T} for some T > 0 and (∂_t + Δ_x)u = f.

Here ℝⁿ⁺¹ has coordinates (x₁, …, xₙ, t) where the last coordinate is time, ∂_t is the distributional derivative in the time direction, and Δ_x is the spatial Laplacian (sum of second derivatives in the first n coordinate directions).

The proof is not given in the textbook, so we axiomatize this result.

def Chapter11.lastCoord (n : ℕ) (x : Rn (n + 1)) : ℝ

Extract the last (time) coordinate of a point in ℝⁿ⁺¹.

noncomputable def Chapter11.timeDir (n : ℕ) : Rn (n + 1)

The unit vector in the time direction (last coordinate) in ℝⁿ⁺¹.

noncomputable def Chapter11.spatialDir (n : ℕ) (i : Fin n) : Rn (n + 1)

The unit vector in the i-th spatial direction in ℝⁿ⁺¹, for i < n.

noncomputable def Chapter11.timeDerivCLM (n : ℕ) : TemperedDistribution (Rn (n + 1)) ℂ →L[ℂ] TemperedDistribution (Rn (n + 1)) ℂ

The distributional time derivative ∂_t on S'(ℝⁿ⁺¹, ℂ), defined as the line derivative in the direction of the last coordinate.

noncomputable def Chapter11.spatialSecondDerivCLM (n : ℕ) (i : Fin n) : TemperedDistribution (Rn (n + 1)) ℂ →L[ℂ] TemperedDistribution (Rn (n + 1)) ℂ

The iterated distributional second derivative ∂²/∂xᵢ² in the i-th spatial direction on S'(ℝⁿ⁺¹, ℂ).

noncomputable def Chapter11.spatialLaplacianCLM (n : ℕ) : TemperedDistribution (Rn (n + 1)) ℂ →L[ℂ] TemperedDistribution (Rn (n + 1)) ℂ

The distributional spatial Laplacian Δ_x = Σᵢ ∂²/∂xᵢ² on S'(ℝⁿ⁺¹, ℂ), where the sum is over the first n (spatial) coordinate directions.

noncomputable def Chapter11.heatOp (n : ℕ) : TemperedDistribution (Rn (n + 1)) ℂ →L[ℂ] TemperedDistribution (Rn (n + 1)) ℂ

The heat operator ∂_t + Δ_x on S'(ℝⁿ⁺¹, ℂ), where ∂_t is the time derivative and Δ_x is the spatial Laplacian.

def Chapter11.HasSupportInFutureHalfSpace (n : ℕ) (T : ℝ) (u : TemperedDistribution (Rn (n + 1)) ℂ) : Prop

A tempered distribution u ∈ S'(ℝⁿ⁺¹, ℂ) has support in the future half-space {t ≥ -T} if u(φ) = 0 for every Schwartz function φ that vanishes identically on the closed half-space {(x, t) : t ≥ -T}. This is the distributional formulation of the condition supp(u) ⊆ {(x, t) ∈ ℝⁿ⁺¹ : t ≥ -T}.

theorem Chapter11.prop_11_16_heat_equation (n : ℕ) (f : TemperedDistribution (Rn (n + 1)) ℂ) (hf : HasCompactDistribSupport f) : ∃ (T : ℝ), ∃! u : TemperedDistribution (Rn (n + 1)) ℂ, HasSupportInFutureHalfSpace n T u ∧ (heatOp n) u = f

Proposition 11.16 (Heat equation existence and uniqueness): If f ∈ S'(ℝⁿ⁺¹) has compact support, then there exists a unique u ∈ S'(ℝⁿ⁺¹) with supp(u) ⊂ {t ≥ -T} for some T and (∂_t + Δ_x)u = f in ℝⁿ⁺¹.

Here (∂_t + Δ_x) is the heat operator, with ∂_t the derivative in the time (last coordinate) direction and Δ_x = Σᵢ ∂²/∂xᵢ² the spatial Laplacian. The support condition means u vanishes for sufficiently negative time.

The proof is not given in the textbook, so we axiomatize this result.

Theorem 11.17: Existence and uniqueness for Δu = f (Goal 91)

The Laplacian Δ on tempered distributions is defined via the Fourier multiplier -(2π)²|ξ|². The equation Δu = f is solved by û(ξ) = -f̂(ξ)/(4π²|ξ|²).

theorem Chapter11.theorem_11_17_laplace_equation (n : ℕ) (s : ℝ) (f : TemperedDistribution (Rn n) ℂ) (hf : MemSobolevSpace n s f) : ∃! u : TemperedDistribution (Rn n) ℂ, MemSobolevSpace n (s + 2) u ∧ Laplacian.laplacian u = f

The proof is not given in the textbook, so we axiomatize it.

Lemma 11.13: Elliptic parametrix

If P_m(ξ) is the principal (homogeneous degree-m) part of a polynomial P and P is elliptic of order m, then Q(ξ) = (1 - φ(ξ)) / P_m(ξ) (with φ a smooth cutoff removing the singularity at the origin) defines a tempered distribution whose inverse Fourier transform F is a parametrix for P_m(D). That is, P_m(D) F = δ + ψ for some ψ ∈ S(ℝⁿ) (equation (11.27)). Moreover, F is smooth away from the origin: sing supp(F) ⊆ {0}.

The proof is not given in the textbook, so this is axiomatized.

noncomputable def Chapter11.principalSymbolOp {n : ℕ} (P : MvPolynomial (Fin n) ℂ) (m : ℕ) : TemperedDistribution (Rn n) ℂ →L[ℂ] TemperedDistribution (Rn n) ℂ

The principal symbol operator P_m(D) for a polynomial P of degree m, acting on tempered distributions over ℝⁿ via the Fourier multiplier P_m(ξ) = evalPolyAtRn n (homogeneousComponent m P) ξ.

On the Fourier side, P_m(D) acts by pointwise multiplication with the principal symbol P_m(ξ), which is a homogeneous polynomial of degree m.

theorem Chapter11.lemma_11_13_elliptic_parametrix {n : ℕ} (P : MvPolynomial (Fin n) ℂ) (m : ℕ) (hP : IsElliptic P m) : ∃ (F : TemperedDistribution (Rn n) ℂ), IsParametrix (Rn n) (principalSymbolOp P m) F ∧ SingularSupport (Rn n) F ⊆ {0}

Lemma 11.13 (Elliptic parametrix): If P_m(ξ) is the principal part (homogeneous component of degree m) of a polynomial P ∈ ℂ[ξ₁,…,ξₙ] and P is elliptic of order m (meaning P_m(ξ) ≠ 0 for all nonzero ξ ∈ ℝⁿ), then the operator P_m(D) admits a parametrix F ∈ S'(ℝⁿ) whose singular support is contained in {0}.

Concretely, the Fourier transform of this parametrix is given by Q(ξ) = (1 - φ(ξ)) / P_m(ξ) where φ is a smooth cutoff equal to 1 near the origin, which removes the singularity at ξ = 0. This defines a tempered distribution satisfying P_m(D)F = δ + ψ where ψ ∈ C^∞(ℝⁿ) (equation (11.27) in the text).

The fact that sing supp(F) ⊆ {0} follows from Q being smooth on ℝⁿ \ {0} (since P_m(ξ) ≠ 0 for ξ ≠ 0 by ellipticity and 1 - φ vanishes near 0).

This is the key step in proving that every elliptic constant-coefficient differential operator is hypoelliptic.

The proof is not given in the textbook, so we axiomatize this result.

Theorem 11.12: Every elliptic differential operator is hypoelliptic

If P(ξ) is an elliptic polynomial of order m (in the sense that the principal part P_m(ξ) ≠ 0 for all nonzero ξ ∈ ℝⁿ), then the associated constant-coefficient differential operator P_m(D) is hypoelliptic: it admits a parametrix F ∈ S'(ℝⁿ) whose singular support is contained in {0}.

This follows directly from Lemma 11.13 (elliptic parametrix), which constructs such a parametrix for the principal symbol operator P_m(D).

theorem Chapter11.theorem_11_12_elliptic_hypoelliptic {n : ℕ} (P : MvPolynomial (Fin n) ℂ) (m : ℕ) (hP : IsElliptic P m) : IsHypoelliptic (Rn n) (principalSymbolOp P m)

Theorem 11.12 (Elliptic implies hypoelliptic): Every elliptic differential operator P(D) is hypoelliptic.

More precisely, let P ∈ ℂ[ξ₁, …, ξₙ] be a polynomial that is elliptic of order m (Definition 11.11). The principal symbol operator P_m(D) (the Fourier multiplier with symbol equal to the homogeneous component of degree m of P) is hypoelliptic (Definition 11.8): there exists a parametrix F ∈ S'(ℝⁿ) satisfying P_m(D)F = δ + ψ (with ψ smooth) whose singular support is contained in {0}.

This is a direct consequence of Lemma 11.13 (elliptic parametrix).