@[reducible, inline]

abbrev HeatEquation.SpaceTime (n : ℕ) : Type

Space-time ℝ^(n+1) for the heat equation, with the time coordinate at index 0 and spatial coordinates at indices 1, …, n.

noncomputable def HeatEquation.timeDirection (n : ℕ) : SpaceTime n

The unit vector in the time direction (index 0) in space-time.

noncomputable def HeatEquation.spatialDirection (n : ℕ) (i : Fin n) : SpaceTime n

The i-th spatial unit vector in space-time (at index i.succ, since 0 is time).

noncomputable def HeatEquation.positiveSpatialLaplacian (n : ℕ) (u : TemperedDistribution (SpaceTime n) ℂ) : TemperedDistribution (SpaceTime n) ℂ

The (positive) spatial Laplacian Δ_x = Σ ∂²/∂xᵢ² acting on tempered distributions on space-time.

noncomputable def HeatEquation.heatOperator (n : ℕ) (u : TemperedDistribution (SpaceTime n) ℂ) : TemperedDistribution (SpaceTime n) ℂ

The heat operator ∂_t - Δ_x acting on tempered distributions on space-time.

def HeatEquation.HasCompactDSupport (n : ℕ) (u : TemperedDistribution (SpaceTime n) ℂ) : Prop

A tempered distribution has compact distributional support if its dsupport is compact.

def HeatEquation.timeCoord (n : ℕ) (x : SpaceTime n) : ℝ

The time coordinate of a space-time point x, i.e. x 0.

def HeatEquation.SupportedInTimeGeq (n : ℕ) (u : TemperedDistribution (SpaceTime n) ℂ) (c : ℝ) : Prop

A tempered distribution u is supported in {t ≥ c} if its distributional support is contained in the half-space {x | timeCoord x ≥ c}.

theorem HeatEquation.isVanishingOn_sub (n : ℕ) {u v : TemperedDistribution (SpaceTime n) ℂ} {s : Set (SpaceTime n)} (hu : Distribution.IsVanishingOn (⇑u) s) (hv : Distribution.IsVanishingOn (⇑v) s) : Distribution.IsVanishingOn (⇑(u - v)) s

IsVanishingOn is preserved by subtraction: if u and v both vanish on s, so does u - v.

theorem HeatEquation.dsupport_sub_subset (n : ℕ) (u v : TemperedDistribution (SpaceTime n) ℂ) : Distribution.dsupport ⇑(u - v) ⊆ Distribution.dsupport ⇑u ∪ Distribution.dsupport ⇑v

The distributional support of u - v is contained in the union of the supports of u and v.

theorem HeatEquation.supportedInTimeGeq_sub (n : ℕ) (u v : TemperedDistribution (SpaceTime n) ℂ) (a b : ℝ) (ha : SupportedInTimeGeq n u a) (hb : SupportedInTimeGeq n v b) : SupportedInTimeGeq n (u - v) (min a b)

If u is supported in {t ≥ a} and v is supported in {t ≥ b}, then u - v is supported in {t ≥ min a b}.

theorem HeatEquation.supportedInTimeGeq_neg (n : ℕ) (u : TemperedDistribution (SpaceTime n) ℂ) (c : ℝ) : SupportedInTimeGeq n (-u) c ↔ SupportedInTimeGeq n u c

SupportedInTimeGeq is invariant under negation of the distribution.

theorem HeatEquation.compact_dsupport_time_bounded_below (n : ℕ) (f : TemperedDistribution (SpaceTime n) ℂ) (hf : HasCompactDSupport n f) : ∃ (b : ℝ), SupportedInTimeGeq n f b

A distribution with compact distributional support is automatically supported in some half-space {t ≥ b}: the time coordinate attains its minimum on a compact set.

noncomputable def HeatEquation.heatKernelFun (n : ℕ) (v : SpaceTime n) : ℝ

The classical heat-kernel density (4πt)^(-n/2) · exp(-|x|²/(4t)) for t > 0, extended by 0 for t ≤ 0.

theorem HeatEquation.heatKernelFun_nonneg (n : ℕ) (v : SpaceTime n) : 0 ≤ heatKernelFun n v

The heat-kernel density is everywhere nonnegative.

theorem HeatEquation.heatKernelFun_eq_zero_of_time_nonpos (n : ℕ) (v : SpaceTime n) (hv : v.ofLp 0 ≤ 0) : heatKernelFun n v = 0

The heat-kernel density vanishes whenever the time coordinate is nonpositive.

noncomputable def HeatEquation.heatKernelMeasure (n : ℕ) : MeasureTheory.Measure (SpaceTime n)

The heat-kernel measure on space-time: the Lebesgue measure weighted by the heat-kernel density.

theorem HeatEquation.heatKernelMeasure_nonpos_eq_zero (n : ℕ) : (heatKernelMeasure n) {v : SpaceTime n | v.ofLp 0 ≤ 0} = 0

The heat-kernel measure assigns measure zero to the half-space {t ≤ 0}.

theorem HeatEquation.heatKernelFun_le_one_of_time_ge_one (n : ℕ) (v : SpaceTime n) (ht : v.ofLp 0 ≥ 1) : heatKernelFun n v ≤ 1

For t ≥ 1, the heat-kernel density is bounded above by 1.

theorem HeatEquation.heatKernelMeasure_le_volume_on_time_ge_one (n : ℕ) : (heatKernelMeasure n).restrict {v : SpaceTime n | v.ofLp 0 ≥ 1} ≤ MeasureTheory.volume.restrict {v : SpaceTime n | v.ofLp 0 ≥ 1}

On the half-space {t ≥ 1}, the heat-kernel measure is dominated by Lebesgue measure (since the density there is at most 1).

theorem HeatEquation.integrable_rexp_neg_mul_sq_norm_euclidean (m : ℕ) {b : ℝ} (hb : 0 < b) : MeasureTheory.Integrable (fun (v : EuclideanSpace ℝ (Fin m)) => Real.exp (-b * ‖v‖ ^ 2)) MeasureTheory.volume

The Gaussian exp(-b·|v|²) on Euclidean space ℝ^m is Lebesgue integrable for any b > 0.

theorem HeatEquation.heatKernelFun_lintegral_time_lt_one (n : ℕ) : ∫⁻ (v : SpaceTime n) in {v : SpaceTime n | 0 < v.ofLp 0 ∧ v.ofLp 0 < 1}, ENNReal.ofReal (heatKernelFun n v) < ⊤

The Lebesgue integral of the heat-kernel density over the time slab {0 < t < 1} is finite.

theorem HeatEquation.heatKernelMeasure_time_lt_one_finite (n : ℕ) : (heatKernelMeasure n) {v : SpaceTime n | v.ofLp 0 < 1} < ⊤

The heat-kernel measure of the half-space {t < 1} is finite.

theorem HeatEquation.heatKernelMeasure_integrable_one_add_norm (n : ℕ) : MeasureTheory.Integrable (fun (x : SpaceTime n) => (1 + ‖x‖) ^ (-↑(n + 2))) (heatKernelMeasure n)

The function (1 + ‖x‖)^(-(n+2)) is integrable with respect to the heat-kernel measure. This provides the temperate growth witness needed to view the heat kernel as a tempered distribution.

instance HeatEquation.heatKernelMeasure_hasTemperateGrowth (n : ℕ) : (heatKernelMeasure n).HasTemperateGrowth

The heat-kernel measure has temperate growth, witnessed by the integrability of (1 + ‖x‖)^(-(n+2)) against it.

noncomputable def HeatEquation.forwardFundSol (n : ℕ) : TemperedDistribution (SpaceTime n) ℂ

The forward fundamental solution of the heat operator: the tempered distribution associated to the heat-kernel measure via the temperate-growth representation.

theorem HeatEquation.heatKernelFun_measurable (n : ℕ) : Measurable (heatKernelFun n)

The heat-kernel density is measurable.

theorem HeatEquation.heatKernelFun_weighted_adjoint_integral_eq (n : ℕ) (φ : SchwartzMap (SpaceTime n) ℂ) : ∫ (v : SpaceTime n), heatKernelFun n v • (-LineDeriv.lineDerivOp (timeDirection n) φ - ∑ i : Fin n, LineDeriv.lineDerivOp (spatialDirection n i) (LineDeriv.lineDerivOp (spatialDirection n i) φ)) v = φ 0

The weighted-integral form of the fundamental-solution identity: integrating the formal adjoint -∂_t - Δ_x applied to a Schwartz function against the heat-kernel density yields φ(0).

theorem HeatEquation.heatKernelMeasure_adjoint_integral_eq (n : ℕ) (φ : SchwartzMap (SpaceTime n) ℂ) : ∫ (x : SpaceTime n), (-LineDeriv.lineDerivOp (timeDirection n) φ - ∑ i : Fin n, LineDeriv.lineDerivOp (spatialDirection n i) (LineDeriv.lineDerivOp (spatialDirection n i) φ)) x ∂heatKernelMeasure n = φ 0

The measure-theoretic form of the fundamental-solution identity: integrating the formal adjoint of the heat operator against φ with respect to the heat-kernel measure equals φ(0).

theorem HeatEquation.heatKernel_adjoint_integral (n : ℕ) (φ : SchwartzMap (SpaceTime n) ℂ) : (forwardFundSol n) (-LineDeriv.lineDerivOp (timeDirection n) φ - ∑ i : Fin n, LineDeriv.lineDerivOp (spatialDirection n i) (LineDeriv.lineDerivOp (spatialDirection n i) φ)) = φ 0

The forward fundamental solution applied to the formal adjoint of the heat operator evaluated at φ yields φ(0).

theorem HeatEquation.forwardFundSol_eq (n : ℕ) : heatOperator n (forwardFundSol n) = TemperedDistribution.delta 0

The forward fundamental solution satisfies the heat-equation distributional identity (∂_t - Δ_x) E = δ₀, identifying E as a fundamental solution of the heat operator.

theorem HeatEquation.forwardFundSol_support (n : ℕ) : SupportedInTimeGeq n (forwardFundSol n) 0

The forward fundamental solution is supported in the forward time half-space {t ≥ 0}, since the heat-kernel density vanishes for t ≤ 0.

noncomputable def HeatEquation.reflConvSchwartzMap (n : ℕ) (v : TemperedDistribution (SpaceTime n) ℂ) (hv : HasCompactDSupport n v) : SchwartzMap (SpaceTime n) ℂ →L[ℂ] SchwartzMap (SpaceTime n) ℂ

The continuous linear map sending a Schwartz function φ to the convolution v * φ (smoothed via the compact-distributional-support convolution construction), packaged as a 𝓢(ℝ^(n+1), ℂ) →L[ℂ] 𝓢(ℝ^(n+1), ℂ) map.

theorem HeatEquation.reflConvSchwartzMap_apply_zero (n : ℕ) (f : TemperedDistribution (SpaceTime n) ℂ) (hf : HasCompactDSupport n f) (φ : SchwartzMap (SpaceTime n) ℂ) : ((reflConvSchwartzMap n f hf) φ) 0 = f φ

Evaluating the reflected convolution reflConvSchwartzMap n f hf φ at the origin recovers f φ.

noncomputable def HeatEquation.dconv (n : ℕ) (u v : TemperedDistribution (SpaceTime n) ℂ) (hv : HasCompactDSupport n v) : TemperedDistribution (SpaceTime n) ℂ

The distributional convolution dconv n u v hv = u * v when v has compact distributional support, defined as the composition of u with the reflected-convolution Schwartz map.

theorem HeatEquation.compactDsupport_conv_fderiv_eq (n : ℕ) (f : TemperedDistribution (SpaceTime n) ℂ) (hf : HasCompactDSupport n f) (m : SpaceTime n) (φ : SchwartzMap (SpaceTime n) ℂ) (x : SpaceTime n) : (fderiv ℝ (⇑(DifferentialOperators.compactDsupportConvolutionSchwartzMap f hf φ)) x) m = f ((SchwartzMap.compSubConstCLM ℂ x) (LineDeriv.lineDerivOp (-m) φ))

The Fréchet derivative of the convolution f * φ is computed via the test-function translation identity.

theorem HeatEquation.reflConvSchwartzMap_comm_lineDerivOp (n : ℕ) (f : TemperedDistribution (SpaceTime n) ℂ) (hf : HasCompactDSupport n f) (m : SpaceTime n) (φ : SchwartzMap (SpaceTime n) ℂ) : (reflConvSchwartzMap n f hf) (LineDeriv.lineDerivOp (-m) φ) = LineDeriv.lineDerivOp m ((reflConvSchwartzMap n f hf) φ)

Commutation of reflConvSchwartzMap with directional derivatives: applying the line derivative ∂_{-m} to φ before convolving equals applying ∂_m after convolving.

theorem HeatEquation.lineDerivOp_dconv (n : ℕ) (u f : TemperedDistribution (SpaceTime n) ℂ) (hf : HasCompactDSupport n f) (m : SpaceTime n) : LineDeriv.lineDerivOp (-m) (dconv n u f hf) = dconv n (LineDeriv.lineDerivOp m u) f hf

The line derivative ∂_{-m} of a distributional convolution dconv n u f hf equals the convolution of ∂_m u with f.

theorem HeatEquation.heatOp_dconv (n : ℕ) (u f : TemperedDistribution (SpaceTime n) ℂ) (hf : HasCompactDSupport n f) : heatOperator n (dconv n u f hf) = dconv n (heatOperator n u) f hf

The heat operator commutes with the distributional convolution: heatOperator (u * f) = (heatOperator u) * f when f has compact distributional support.

theorem HeatEquation.delta_dconv (n : ℕ) (f : TemperedDistribution (SpaceTime n) ℂ) (hf : HasCompactDSupport n f) : dconv n (TemperedDistribution.delta 0) f hf = f

The Dirac delta at the origin is the identity for distributional convolution: δ₀ * f = f for any f with compact distributional support.

theorem HeatEquation.isVanishingOn_compl_of_dsupport_subset (n : ℕ) (u : TemperedDistribution (SpaceTime n) ℂ) (S : Set (SpaceTime n)) (hS : IsClosed S) (h : Distribution.dsupport ⇑u ⊆ S) : Distribution.IsVanishingOn (⇑u) Sᶜ

If the distributional support of u is contained in a closed set S, then u vanishes on the open complement Sᶜ (in the sense that u φ = 0 whenever tsupport φ ⊆ Sᶜ).

theorem HeatEquation.reflConvSchwartzMap_tsupport_subset (n : ℕ) (f : TemperedDistribution (SpaceTime n) ℂ) (hf : HasCompactDSupport n f) (a b : ℝ) (hb : SupportedInTimeGeq n f b) (φ : SchwartzMap (SpaceTime n) ℂ) (hφ : tsupport ⇑φ ⊆ {x : SpaceTime n | timeCoord n x < a + b}) : tsupport ⇑((reflConvSchwartzMap n f hf) φ) ⊆ {x : SpaceTime n | timeCoord n x < a}

Support property of the reflected-convolution Schwartz map: if f is supported in {t ≥ b} and φ has time support in {t < a + b}, then the convolution reflConvSchwartzMap n f hf φ has time support in {t < a}.

theorem HeatEquation.reflConvSchwartzMap_isVanishingOn (n : ℕ) (u f : TemperedDistribution (SpaceTime n) ℂ) (hf : HasCompactDSupport n f) (a b : ℝ) (ha : SupportedInTimeGeq n u a) (hb : SupportedInTimeGeq n f b) (φ : SchwartzMap (SpaceTime n) ℂ) : tsupport ⇑φ ⊆ {x : SpaceTime n | timeCoord n x < a + b} → u ((reflConvSchwartzMap n f hf) φ) = 0

If u is supported in {t ≥ a} and f is supported in {t ≥ b}, then u vanishes on the convolution reflConvSchwartzMap n f hf φ whenever φ has time support in {t < a + b}.

theorem HeatEquation.dconv_support_timeGeq (n : ℕ) (u f : TemperedDistribution (SpaceTime n) ℂ) (hf : HasCompactDSupport n f) (a b : ℝ) (ha : SupportedInTimeGeq n u a) (hb : SupportedInTimeGeq n f b) : SupportedInTimeGeq n (dconv n u f hf) (a + b)

Support additivity for the distributional convolution: if u is supported in {t ≥ a} and f in {t ≥ b}, then dconv n u f hf is supported in {t ≥ a + b}.

theorem HeatEquation.cutoffHeatKernel_identity (n : ℕ) (s : ℝ) : ∃ (E_s : TemperedDistribution (SpaceTime n) ℂ) (hE_s : HasCompactDSupport n E_s) (ψ : TemperedDistribution (SpaceTime n) ℂ) (hψ : HasCompactDSupport n ψ), SupportedInTimeGeq n ψ s ∧ ∀ (v : TemperedDistribution (SpaceTime n) ℂ), heatOperator n (dconv n v E_s hE_s) = v + dconv n v ψ hψ

Cutoff heat-kernel identity: there exists a cutoff E_s of the forward fundamental solution with compact distributional support and an "error" distribution ψ (supported in {t ≥ s}) such that the heat operator applied to the convolution v * E_s equals v + v * ψ for all v. This is a key technical tool for the uniqueness argument in Prop 11.16.

theorem HeatEquation.cutoffPerturbation_exists (n : ℕ) (s : ℝ) : ∃ (ψ : TemperedDistribution (SpaceTime n) ℂ) (hψ : HasCompactDSupport n ψ), SupportedInTimeGeq n ψ s ∧ ∀ (v : TemperedDistribution (SpaceTime n) ℂ), heatOperator n v = 0 → v + dconv n v ψ hψ = 0

Cutoff perturbation identity for homogeneous heat solutions: for every s, there is a distribution ψ (with compact distributional support, supported in {t ≥ s}) such that any solution v of the homogeneous heat equation satisfies v + v * ψ = 0.

theorem HeatEquation.heat_homogeneous_support_shift (n : ℕ) (v : TemperedDistribution (SpaceTime n) ℂ) (hv_eq : heatOperator n v = 0) (T' s : ℝ) (hsupp : SupportedInTimeGeq n v T') : SupportedInTimeGeq n v (T' + s)

Support-shift lemma for homogeneous heat solutions: a homogeneous solution v whose support lies in {t ≥ T'} is in fact supported in {t ≥ T' + s} for every s. Iterating this drives the support to ∅, yielding uniqueness.

theorem HeatEquation.dsupport_eq_empty_imp_eq_zero (n : ℕ) (v : TemperedDistribution (SpaceTime n) ℂ) (h : Distribution.dsupport ⇑v = ∅) : v = 0

A tempered distribution with empty distributional support is the zero distribution.

theorem HeatEquation.heat_homogeneous_uniqueness (n : ℕ) (v : TemperedDistribution (SpaceTime n) ℂ) (hv_eq : heatOperator n v = 0) (hv_supp : ∃ (T' : ℝ), SupportedInTimeGeq n v T') : v = 0

Uniqueness statement for the homogeneous heat equation: any solution v of (∂_t - Δ_x) v = 0 whose distributional support is bounded below in time must vanish.

theorem HeatEquation.heatOperator_sub (n : ℕ) (u v : TemperedDistribution (SpaceTime n) ℂ) : heatOperator n (u - v) = heatOperator n u - heatOperator n v

The heat operator is linear, in particular `heatOperator (u - v) = heatOperator u

• heatOperator v`.

theorem HeatEquation.heat_equation_existence_uniqueness (n : ℕ) (f : TemperedDistribution (SpaceTime n) ℂ) (hf : HasCompactDSupport n f) : ∃! u : TemperedDistribution (SpaceTime n) ℂ, (∃ (T : ℝ), SupportedInTimeGeq n u (-T)) ∧ heatOperator n u = f

Proposition 11.16 (existence and uniqueness for the heat equation): for every tempered distribution f with compact distributional support, there is a unique tempered distribution u, bounded below in time, satisfying (∂_t - Δ_x) u = f.