The weak maximum principle for the heat equation

Let K be a compact subset of a finite-dimensional real inner product space E and T a time. On the space-time cylinder [0, T] × K consider the parabolic operator

∂ₜu - Δu - b·∇u,

with a time-dependent drift field b : ℝ → E → E; for b = 0 this is the heat operator. A function u : ℝ → E → ℝ (time first, so u t is the spatial slice at time t) is a subsolution when ∂ₜu ≤ Δu + b·∇u at every point of the open cylinder (0, T) × interior K. In Lean the drift term ⟪b, ∇u⟫ is spelled fderiv ℝ (u t) x (b t x), as in TauCeti.Analysis.InnerProductSpace.Laplacian.DriftMaximumPrinciple.

The parabolic boundary of the cylinder is its bottom {0} × K together with its lateral side [0, T] × frontier K; the top {T} × interior K is not part of it. The weak maximum principle says that a subsolution which is continuous on the closed cylinder is bounded on the whole cylinder by any bound it satisfies on the parabolic boundary.

The proof is the classical one. For ε > 0 the function u - εt is a strict subsolution, so it cannot attain its maximum over [0, τ] × K (for τ < T) at a point (t₀, x₀) with t₀ > 0 and x₀ ∈ interior K: there Δ(u t₀) x₀ ≤ 0 and ∇(u t₀) x₀ = 0 because x₀ is a spatial local maximum, while ∂ₜu(t₀, x₀) ≥ ε because t₀ is a maximum from the left. Letting ε → 0 gives the bound for t < T, and continuity carries it to the top t = T. Unlike the elliptic principle for Δ + b·∇, no bound on the drift is needed, because the perturbation εt does not depend on the space variable.

Regularity is only required on the open cylinder (0, T) × interior K (C² in space, differentiable in time), together with continuity on the closed cylinder [0, T] × K.

Main declarations

• TauCeti.le_of_deriv_le_laplacian_add_fderiv_le_parabolicBoundary: the weak maximum principle for ∂ₜ - Δ - b·∇, in bound form.
• TauCeti.le_of_deriv_le_laplacian_le_parabolicBoundary: its case b = 0, the weak maximum principle for subsolutions of the heat equation ∂ₜu ≤ Δu.
• TauCeti.ge_of_laplacian_add_fderiv_le_deriv_ge_parabolicBoundary: the weak minimum principle for supersolutions.
• TauCeti.le_of_deriv_sub_laplacian_sub_fderiv_le_of_le_parabolicBoundary: the comparison principle.
• TauCeti.eqOn_of_deriv_sub_laplacian_sub_fderiv_eq_of_eqOn_parabolicBoundary: uniqueness for the initial-boundary value problem ∂ₜu - Δu - b·∇u = f, u = g on the parabolic boundary.
• TauCeti.ge_of_laplacian_le_deriv_ge_parabolicBoundary, TauCeti.le_of_deriv_sub_laplacian_le_of_le_parabolicBoundary, TauCeti.eqOn_of_deriv_sub_laplacian_eq_of_eqOn_parabolicBoundary: the minimum principle, comparison principle and uniqueness for the heat equation (b = 0).

References

• L. C. Evans, Partial Differential Equations, Section 2.3.3, Theorems 4 (i) and 5, and Section 7.1.4, Theorem 8.

theorem TauCeti.le_of_deriv_le_laplacian_add_fderiv_le_parabolicBoundary {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {K : Set E} {T : ℝ} {u : ℝ → E → ℝ} {b : ℝ → E → E} (hK : IsCompact K) {m : ℝ} (hcont : ContinuousOn (Function.uncurry u) (Set.Icc 0 T ×ˢ K)) (hcd : ∀ ⦃t : ℝ⦄, t ∈ Set.Ioo 0 T → ∀ ⦃x : E⦄, x ∈ interior K → ContDiffAt ℝ 2 (u t) x) (hdiff : ∀ ⦃t : ℝ⦄, t ∈ Set.Ioo 0 T → ∀ ⦃x : E⦄, x ∈ interior K → DifferentiableAt ℝ (fun (s : ℝ) => u s x) t) (hsub : ∀ ⦃t : ℝ⦄, t ∈ Set.Ioo 0 T → ∀ ⦃x : E⦄, x ∈ interior K → deriv (fun (s : ℝ) => u s x) t ≤ Laplacian.laplacian (u t) x + (fderiv ℝ (u t) x) (b t x)) (hinit : ∀ ⦃x : E⦄, x ∈ K → u 0 x ≤ m) (hlat : ∀ ⦃t : ℝ⦄, t ∈ Set.Icc 0 T → ∀ ⦃x : E⦄, x ∈ frontier K → u t x ≤ m) ⦃t : ℝ⦄ : t ∈ Set.Icc 0 T → ∀ ⦃x : E⦄, x ∈ K → u t x ≤ m

Weak maximum principle for ∂ₜ - Δ - b·∇.

Let K be compact. Suppose u is continuous on the closed cylinder [0, T] × K, is C² in space and differentiable in time on the open cylinder (0, T) × interior K, and is a subsolution there: ∂ₜu ≤ Δu + b·∇u. If u ≤ m on the parabolic boundary, that is on the bottom {0} × K and on the lateral side [0, T] × frontier K, then u ≤ m on all of [0, T] × K. No bound on the drift b is needed.

theorem TauCeti.le_of_deriv_le_laplacian_le_parabolicBoundary {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {K : Set E} {T : ℝ} {u : ℝ → E → ℝ} (hK : IsCompact K) {m : ℝ} (hcont : ContinuousOn (Function.uncurry u) (Set.Icc 0 T ×ˢ K)) (hcd : ∀ ⦃t : ℝ⦄, t ∈ Set.Ioo 0 T → ∀ ⦃x : E⦄, x ∈ interior K → ContDiffAt ℝ 2 (u t) x) (hdiff : ∀ ⦃t : ℝ⦄, t ∈ Set.Ioo 0 T → ∀ ⦃x : E⦄, x ∈ interior K → DifferentiableAt ℝ (fun (s : ℝ) => u s x) t) (hsub : ∀ ⦃t : ℝ⦄, t ∈ Set.Ioo 0 T → ∀ ⦃x : E⦄, x ∈ interior K → deriv (fun (s : ℝ) => u s x) t ≤ Laplacian.laplacian (u t) x) (hinit : ∀ ⦃x : E⦄, x ∈ K → u 0 x ≤ m) (hlat : ∀ ⦃t : ℝ⦄, t ∈ Set.Icc 0 T → ∀ ⦃x : E⦄, x ∈ frontier K → u t x ≤ m) ⦃t : ℝ⦄ : t ∈ Set.Icc 0 T → ∀ ⦃x : E⦄, x ∈ K → u t x ≤ m

Weak maximum principle for the heat equation. A subsolution ∂ₜu ≤ Δu of the heat equation, continuous on the closed cylinder [0, T] × K over a compact K and regular on the open cylinder (0, T) × interior K, is bounded on [0, T] × K by any bound it satisfies on the parabolic boundary ({0} × K) ∪ ([0, T] × frontier K).

theorem TauCeti.ge_of_laplacian_add_fderiv_le_deriv_ge_parabolicBoundary {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {K : Set E} {T : ℝ} {u : ℝ → E → ℝ} {b : ℝ → E → E} (hK : IsCompact K) {m : ℝ} (hcont : ContinuousOn (Function.uncurry u) (Set.Icc 0 T ×ˢ K)) (hcd : ∀ ⦃t : ℝ⦄, t ∈ Set.Ioo 0 T → ∀ ⦃x : E⦄, x ∈ interior K → ContDiffAt ℝ 2 (u t) x) (hdiff : ∀ ⦃t : ℝ⦄, t ∈ Set.Ioo 0 T → ∀ ⦃x : E⦄, x ∈ interior K → DifferentiableAt ℝ (fun (s : ℝ) => u s x) t) (hsuper : ∀ ⦃t : ℝ⦄, t ∈ Set.Ioo 0 T → ∀ ⦃x : E⦄, x ∈ interior K → Laplacian.laplacian (u t) x + (fderiv ℝ (u t) x) (b t x) ≤ deriv (fun (s : ℝ) => u s x) t) (hinit : ∀ ⦃x : E⦄, x ∈ K → m ≤ u 0 x) (hlat : ∀ ⦃t : ℝ⦄, t ∈ Set.Icc 0 T → ∀ ⦃x : E⦄, x ∈ frontier K → m ≤ u t x) ⦃t : ℝ⦄ : t ∈ Set.Icc 0 T → ∀ ⦃x : E⦄, x ∈ K → m ≤ u t x

Weak minimum principle for ∂ₜ - Δ - b·∇. The dual of le_of_deriv_le_laplacian_add_fderiv_le_parabolicBoundary for supersolutions (Δu + b·∇u ≤ ∂ₜu): any lower bound on the parabolic boundary holds on all of [0, T] × K.

theorem TauCeti.ge_of_laplacian_le_deriv_ge_parabolicBoundary {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {K : Set E} {T : ℝ} {u : ℝ → E → ℝ} (hK : IsCompact K) {m : ℝ} (hcont : ContinuousOn (Function.uncurry u) (Set.Icc 0 T ×ˢ K)) (hcd : ∀ ⦃t : ℝ⦄, t ∈ Set.Ioo 0 T → ∀ ⦃x : E⦄, x ∈ interior K → ContDiffAt ℝ 2 (u t) x) (hdiff : ∀ ⦃t : ℝ⦄, t ∈ Set.Ioo 0 T → ∀ ⦃x : E⦄, x ∈ interior K → DifferentiableAt ℝ (fun (s : ℝ) => u s x) t) (hsuper : ∀ ⦃t : ℝ⦄, t ∈ Set.Ioo 0 T → ∀ ⦃x : E⦄, x ∈ interior K → Laplacian.laplacian (u t) x ≤ deriv (fun (s : ℝ) => u s x) t) (hinit : ∀ ⦃x : E⦄, x ∈ K → m ≤ u 0 x) (hlat : ∀ ⦃t : ℝ⦄, t ∈ Set.Icc 0 T → ∀ ⦃x : E⦄, x ∈ frontier K → m ≤ u t x) ⦃t : ℝ⦄ : t ∈ Set.Icc 0 T → ∀ ⦃x : E⦄, x ∈ K → m ≤ u t x

Weak minimum principle for the heat equation. A supersolution Δu ≤ ∂ₜu of the heat equation, continuous on the closed cylinder [0, T] × K over a compact K and regular on the open cylinder (0, T) × interior K, satisfies on [0, T] × K any lower bound it satisfies on the parabolic boundary ({0} × K) ∪ ([0, T] × frontier K).

theorem TauCeti.le_of_deriv_sub_laplacian_sub_fderiv_le_of_le_parabolicBoundary {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {K : Set E} {T : ℝ} {u : ℝ → E → ℝ} {b : ℝ → E → E} (hK : IsCompact K) {v : ℝ → E → ℝ} (hucont : ContinuousOn (Function.uncurry u) (Set.Icc 0 T ×ˢ K)) (hvcont : ContinuousOn (Function.uncurry v) (Set.Icc 0 T ×ˢ K)) (hucd : ∀ ⦃t : ℝ⦄, t ∈ Set.Ioo 0 T → ∀ ⦃x : E⦄, x ∈ interior K → ContDiffAt ℝ 2 (u t) x) (hvcd : ∀ ⦃t : ℝ⦄, t ∈ Set.Ioo 0 T → ∀ ⦃x : E⦄, x ∈ interior K → ContDiffAt ℝ 2 (v t) x) (hudiff : ∀ ⦃t : ℝ⦄, t ∈ Set.Ioo 0 T → ∀ ⦃x : E⦄, x ∈ interior K → DifferentiableAt ℝ (fun (s : ℝ) => u s x) t) (hvdiff : ∀ ⦃t : ℝ⦄, t ∈ Set.Ioo 0 T → ∀ ⦃x : E⦄, x ∈ interior K → DifferentiableAt ℝ (fun (s : ℝ) => v s x) t) (hL : ∀ ⦃t : ℝ⦄, t ∈ Set.Ioo 0 T → ∀ ⦃x : E⦄, x ∈ interior K → deriv (fun (s : ℝ) => u s x) t - (Laplacian.laplacian (u t) x + (fderiv ℝ (u t) x) (b t x)) ≤ deriv (fun (s : ℝ) => v s x) t - (Laplacian.laplacian (v t) x + (fderiv ℝ (v t) x) (b t x))) (hinit : ∀ ⦃x : E⦄, x ∈ K → u 0 x ≤ v 0 x) (hlat : ∀ ⦃t : ℝ⦄, t ∈ Set.Icc 0 T → ∀ ⦃x : E⦄, x ∈ frontier K → u t x ≤ v t x) ⦃t : ℝ⦄ : t ∈ Set.Icc 0 T → ∀ ⦃x : E⦄, x ∈ K → u t x ≤ v t x

Comparison principle for ∂ₜ - Δ - b·∇. If (∂ₜ - Δ - b·∇) u ≤ (∂ₜ - Δ - b·∇) v on the open cylinder (0, T) × interior K and u ≤ v on the parabolic boundary, then u ≤ v on all of [0, T] × K.

theorem TauCeti.le_of_deriv_sub_laplacian_le_of_le_parabolicBoundary {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {K : Set E} {T : ℝ} {u : ℝ → E → ℝ} (hK : IsCompact K) {v : ℝ → E → ℝ} (hucont : ContinuousOn (Function.uncurry u) (Set.Icc 0 T ×ˢ K)) (hvcont : ContinuousOn (Function.uncurry v) (Set.Icc 0 T ×ˢ K)) (hucd : ∀ ⦃t : ℝ⦄, t ∈ Set.Ioo 0 T → ∀ ⦃x : E⦄, x ∈ interior K → ContDiffAt ℝ 2 (u t) x) (hvcd : ∀ ⦃t : ℝ⦄, t ∈ Set.Ioo 0 T → ∀ ⦃x : E⦄, x ∈ interior K → ContDiffAt ℝ 2 (v t) x) (hudiff : ∀ ⦃t : ℝ⦄, t ∈ Set.Ioo 0 T → ∀ ⦃x : E⦄, x ∈ interior K → DifferentiableAt ℝ (fun (s : ℝ) => u s x) t) (hvdiff : ∀ ⦃t : ℝ⦄, t ∈ Set.Ioo 0 T → ∀ ⦃x : E⦄, x ∈ interior K → DifferentiableAt ℝ (fun (s : ℝ) => v s x) t) (hL : ∀ ⦃t : ℝ⦄, t ∈ Set.Ioo 0 T → ∀ ⦃x : E⦄, x ∈ interior K → deriv (fun (s : ℝ) => u s x) t - Laplacian.laplacian (u t) x ≤ deriv (fun (s : ℝ) => v s x) t - Laplacian.laplacian (v t) x) (hinit : ∀ ⦃x : E⦄, x ∈ K → u 0 x ≤ v 0 x) (hlat : ∀ ⦃t : ℝ⦄, t ∈ Set.Icc 0 T → ∀ ⦃x : E⦄, x ∈ frontier K → u t x ≤ v t x) ⦃t : ℝ⦄ : t ∈ Set.Icc 0 T → ∀ ⦃x : E⦄, x ∈ K → u t x ≤ v t x

Comparison principle for the heat equation. If ∂ₜu - Δu ≤ ∂ₜv - Δv on the open cylinder (0, T) × interior K and u ≤ v on the parabolic boundary, then u ≤ v on all of [0, T] × K.

theorem TauCeti.eqOn_of_deriv_sub_laplacian_sub_fderiv_eq_of_eqOn_parabolicBoundary {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {K : Set E} {T : ℝ} {u : ℝ → E → ℝ} {b : ℝ → E → E} (hK : IsCompact K) {v : ℝ → E → ℝ} (hucont : ContinuousOn (Function.uncurry u) (Set.Icc 0 T ×ˢ K)) (hvcont : ContinuousOn (Function.uncurry v) (Set.Icc 0 T ×ˢ K)) (hucd : ∀ ⦃t : ℝ⦄, t ∈ Set.Ioo 0 T → ∀ ⦃x : E⦄, x ∈ interior K → ContDiffAt ℝ 2 (u t) x) (hvcd : ∀ ⦃t : ℝ⦄, t ∈ Set.Ioo 0 T → ∀ ⦃x : E⦄, x ∈ interior K → ContDiffAt ℝ 2 (v t) x) (hudiff : ∀ ⦃t : ℝ⦄, t ∈ Set.Ioo 0 T → ∀ ⦃x : E⦄, x ∈ interior K → DifferentiableAt ℝ (fun (s : ℝ) => u s x) t) (hvdiff : ∀ ⦃t : ℝ⦄, t ∈ Set.Ioo 0 T → ∀ ⦃x : E⦄, x ∈ interior K → DifferentiableAt ℝ (fun (s : ℝ) => v s x) t) (hL : ∀ ⦃t : ℝ⦄, t ∈ Set.Ioo 0 T → ∀ ⦃x : E⦄, x ∈ interior K → deriv (fun (s : ℝ) => u s x) t - (Laplacian.laplacian (u t) x + (fderiv ℝ (u t) x) (b t x)) = deriv (fun (s : ℝ) => v s x) t - (Laplacian.laplacian (v t) x + (fderiv ℝ (v t) x) (b t x))) (hinit : Set.EqOn (u 0) (v 0) K) (hlat : ∀ ⦃t : ℝ⦄, t ∈ Set.Icc 0 T → Set.EqOn (u t) (v t) (frontier K)) : Set.EqOn (Function.uncurry u) (Function.uncurry v) (Set.Icc 0 T ×ˢ K)

Uniqueness for the initial-boundary value problem of ∂ₜ - Δ - b·∇. Two functions with equal values of ∂ₜ - Δ - b·∇ on the open cylinder (0, T) × interior K and equal values on the parabolic boundary agree on all of [0, T] × K.

theorem TauCeti.eqOn_of_deriv_sub_laplacian_eq_of_eqOn_parabolicBoundary {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {K : Set E} {T : ℝ} {u : ℝ → E → ℝ} (hK : IsCompact K) {v : ℝ → E → ℝ} (hucont : ContinuousOn (Function.uncurry u) (Set.Icc 0 T ×ˢ K)) (hvcont : ContinuousOn (Function.uncurry v) (Set.Icc 0 T ×ˢ K)) (hucd : ∀ ⦃t : ℝ⦄, t ∈ Set.Ioo 0 T → ∀ ⦃x : E⦄, x ∈ interior K → ContDiffAt ℝ 2 (u t) x) (hvcd : ∀ ⦃t : ℝ⦄, t ∈ Set.Ioo 0 T → ∀ ⦃x : E⦄, x ∈ interior K → ContDiffAt ℝ 2 (v t) x) (hudiff : ∀ ⦃t : ℝ⦄, t ∈ Set.Ioo 0 T → ∀ ⦃x : E⦄, x ∈ interior K → DifferentiableAt ℝ (fun (s : ℝ) => u s x) t) (hvdiff : ∀ ⦃t : ℝ⦄, t ∈ Set.Ioo 0 T → ∀ ⦃x : E⦄, x ∈ interior K → DifferentiableAt ℝ (fun (s : ℝ) => v s x) t) (hL : ∀ ⦃t : ℝ⦄, t ∈ Set.Ioo 0 T → ∀ ⦃x : E⦄, x ∈ interior K → deriv (fun (s : ℝ) => u s x) t - Laplacian.laplacian (u t) x = deriv (fun (s : ℝ) => v s x) t - Laplacian.laplacian (v t) x) (hinit : Set.EqOn (u 0) (v 0) K) (hlat : ∀ ⦃t : ℝ⦄, t ∈ Set.Icc 0 T → Set.EqOn (u t) (v t) (frontier K)) : Set.EqOn (Function.uncurry u) (Function.uncurry v) (Set.Icc 0 T ×ˢ K)

Uniqueness for the initial-boundary value problem of the heat equation. Two functions with equal values of ∂ₜ - Δ on the open cylinder (0, T) × interior K and equal values on the parabolic boundary agree on all of [0, T] × K.