@[reducible, inline]

abbrev DifferentialOperators.SpaceTime (n : ℕ) : Type

The (n + 1)-dimensional spacetime ℝ^{1+n}, with the first coordinate playing the role of time and the remaining n coordinates the spatial ones.

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

The unit vector in the time direction of SpaceTime n.

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

The unit vector in the i-th spatial direction of SpaceTime n.

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

The positive spatial Laplacian acting on tempered distributions on SpaceTime n: Σᵢ ∂ᵢ² summed over the spatial directions.

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

The heat operator ∂ₜ − Δ on tempered distributions on SpaceTime n.

def DifferentialOperators.DistributionVanishesOn (n : ℕ) (u : TemperedDistribution (SpaceTime n) ℂ) (U : Set (SpaceTime n)) : Prop

A tempered distribution u vanishes on an open set U if it pairs to zero with every Schwartz function whose support is contained in U.

def DifferentialOperators.distributionalSupport (n : ℕ) (u : TemperedDistribution (SpaceTime n) ℂ) : Set (SpaceTime n)

The distributional support of u: the set of points without any open neighbourhood on which u vanishes (i.e., the complement of the largest open set on which u vanishes).

def DifferentialOperators.HasCompactDistributionalSupport (n : ℕ) (u : TemperedDistribution (SpaceTime n) ℂ) : Prop

A tempered distribution has compact distributional support iff its distributional support is a compact set.

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

The time coordinate (first component) of a point in SpaceTime n.

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

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

theorem DifferentialOperators.distributionVanishesOn_sub (n : ℕ) {u v : TemperedDistribution (SpaceTime n) ℂ} {U : Set (SpaceTime n)} (hu : DistributionVanishesOn n u U) (hv : DistributionVanishesOn n v U) : DistributionVanishesOn n (u - v) U

If two tempered distributions both vanish on an open set U, so does their difference.

theorem DifferentialOperators.distributionalSupport_sub_subset (n : ℕ) (u v : TemperedDistribution (SpaceTime n) ℂ) : distributionalSupport n (u - v) ⊆ distributionalSupport n u ∪ distributionalSupport n v

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

theorem DifferentialOperators.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 DifferentialOperators.compact_support_time_bounded_below (n : ℕ) (f : TemperedDistribution (SpaceTime n) ℂ) (hf : HasCompactDistributionalSupport n f) : ∃ (b : ℝ), SupportedInTimeGeq n f b

A distribution with compact distributional support is supported in some half-space {t ≥ b} (i.e. has a lower time bound).

noncomputable def DifferentialOperators.forwardFundamentalSolution (n : ℕ) : TemperedDistribution (SpaceTime n) ℂ

The forward fundamental solution of the heat operator on SpaceTime n: a tempered distribution E such that (∂ₜ − Δ) E = δ₀ and E is supported in {t ≥ 0}.

theorem DifferentialOperators.forwardFundamentalSolution_eq (n : ℕ) : heatOperator n (forwardFundamentalSolution n) = TemperedDistribution.delta 0

Defining property of the forward fundamental solution: applying the heat operator returns the Dirac delta at the origin.

theorem DifferentialOperators.forwardFundamentalSolution_support (n : ℕ) : SupportedInTimeGeq n (forwardFundamentalSolution n) 0

The forward fundamental solution of the heat operator is supported in the forward time half-space {t ≥ 0}.

noncomputable def DifferentialOperators.distributionConvolution (n : ℕ) (u v : TemperedDistribution (SpaceTime n) ℂ) (hv : HasCompactDistributionalSupport n v) : TemperedDistribution (SpaceTime n) ℂ

Convolution u * v of two tempered distributions, defined whenever v has compact distributional support.

theorem DifferentialOperators.heatOperator_convolution (n : ℕ) (u f : TemperedDistribution (SpaceTime n) ℂ) (hf : HasCompactDistributionalSupport n f) : heatOperator n (distributionConvolution n u f hf) = distributionConvolution n (heatOperator n u) f hf

The heat operator commutes with convolution against a compactly supported distribution: (∂ₜ − Δ)(u * f) = ((∂ₜ − Δ)u) * f.

theorem DifferentialOperators.delta_convolution (n : ℕ) (f : TemperedDistribution (SpaceTime n) ℂ) (hf : HasCompactDistributionalSupport n f) : distributionConvolution n (TemperedDistribution.delta 0) f hf = f

Convolution by the Dirac delta at the origin is the identity.

theorem DifferentialOperators.convolution_support_timeGeq (n : ℕ) (u f : TemperedDistribution (SpaceTime n) ℂ) (hf : HasCompactDistributionalSupport n f) (a b : ℝ) (ha : SupportedInTimeGeq n u a) (hb : SupportedInTimeGeq n f b) : SupportedInTimeGeq n (distributionConvolution n u f hf) (a + b)

Time supports add under convolution: if u is supported in {t ≥ a} and f is supported in {t ≥ b}, then u * f is supported in {t ≥ a + b}.

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

Uniqueness for the homogeneous heat equation under a one-sided time support condition: if (∂ₜ − Δ) v = 0 as a tempered distribution and v is supported in some forward half-space {t ≥ T'}, then v = 0.

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

The heat operator distributes over subtraction: (∂ₜ − Δ)(u − v) = (∂ₜ − Δ)u − (∂ₜ − Δ)v.