def WeakMaximumPrinciple.SpacetimeCylinder (T a b : ℝ) : Set (ℝ × ℝ)

The open spacetime cylinder $Q_T = (0,T) \times (a,b) \subseteq \mathbb{R}^2$, the spatial-temporal domain on which the heat equation is posed.

def WeakMaximumPrinciple.ClosedCylinder (T a b : ℝ) : Set (ℝ × ℝ)

The closed spacetime cylinder $\overline{Q_T} = [0,T] \times [a,b]$, the closure of the spacetime cylinder where the solution is required to be continuous.

def WeakMaximumPrinciple.ParabolicBoundary (T a b : ℝ) : Set (ℝ × ℝ)

The parabolic boundary $\partial_p Q_T = (\{0\} \times [a,b]) \cup ((0,T] \times \{a,b\})$, i.e. the bottom of the cylinder together with its lateral sides (but not the top).

theorem WeakMaximumPrinciple.ParabolicBoundary_subset_ClosedCylinder {T a b : ℝ} (hT : 0 < T) (hab : a ≤ b) : ParabolicBoundary T a b ⊆ ClosedCylinder T a b

The parabolic boundary is contained in the closed cylinder.

theorem WeakMaximumPrinciple.ClosedCylinder_nonempty {T a b : ℝ} (hT : 0 ≤ T) (hab : a ≤ b) : (ClosedCylinder T a b).Nonempty

The closed cylinder is nonempty whenever $T \ge 0$ and $a \le b$.

theorem WeakMaximumPrinciple.ParabolicBoundary_nonempty {T a b : ℝ} (hab : a ≤ b) : (ParabolicBoundary T a b).Nonempty

The parabolic boundary is nonempty whenever $a \le b$ (it contains $(0, a)$).

theorem WeakMaximumPrinciple.ClosedCylinder_isCompact {T a b : ℝ} : IsCompact (ClosedCylinder T a b)

The closed cylinder $[0,T] \times [a,b]$ is compact, as a product of compact intervals.

noncomputable def WeakMaximumPrinciple.HeatOp (u : ℝ × ℝ → ℝ) (D : ℝ) (p : ℝ × ℝ) : ℝ

The heat operator $L_D u = u_t - D \, u_{xx}$ acting on a function $u : \mathbb{R}^2 \to \mathbb{R}$ at a point $p = (t, x)$, with diffusion constant $D$.

theorem WeakMaximumPrinciple.HeatOp_fderiv_sub_const_eq (f : ℝ → ℝ) (c x : ℝ) : fderiv ℝ (fun (t : ℝ) => f t - c) x = fderiv ℝ f x

Subtracting a constant does not change the Fréchet derivative: $\frac{d}{dx}(f(x) - c) = \frac{d}{dx} f(x)$.

theorem WeakMaximumPrinciple.time_deriv_nonneg_at_interior_max {T a b : ℝ} (hT : 0 < T) (hab : a < b) (u : ℝ × ℝ → ℝ) (hu_cont : ContinuousOn u (ClosedCylinder T a b)) (t₀ x₀ : ℝ) (ht₀ : 0 < t₀) (ht₀T : t₀ ≤ T) (hx₀a : a < x₀) (hx₀b : x₀ < b) (hmax : ∀ q ∈ ClosedCylinder T a b, u q ≤ u (t₀, x₀)) : (fderiv ℝ (fun (t : ℝ) => u (t, x₀)) t₀) 1 ≥ 0

At an interior maximum point $(t_0, x_0)$ of $u$ in the closed cylinder (with $t_0 > 0$ and $a < x_0 < b$), the time derivative satisfies $u_t(t_0, x_0) \ge 0$, since $u$ does not increase as $t$ decreases away from the maximum.

theorem WeakMaximumPrinciple.spatial_second_deriv_nonpos_at_interior_max {T a b : ℝ} (hT : 0 < T) (hab : a < b) (u : ℝ × ℝ → ℝ) (hu_cont : ContinuousOn u (ClosedCylinder T a b)) (t₀ x₀ : ℝ) (ht₀ : 0 < t₀) (ht₀T : t₀ ≤ T) (hx₀a : a < x₀) (hx₀b : x₀ < b) (hmax : ∀ q ∈ ClosedCylinder T a b, u q ≤ u (t₀, x₀)) : (fderiv ℝ (fun (x : ℝ) => (fderiv ℝ (fun (x' : ℝ) => u (t₀, x')) x) 1) x₀) 1 ≤ 0

At an interior maximum point $(t_0, x_0)$ of $u$ (with $a < x_0 < b$), the second spatial derivative satisfies $u_{xx}(t_0, x_0) \le 0$, by the standard one-variable second derivative test.

theorem WeakMaximumPrinciple.interior_max_HeatOp_nonneg {T a b D : ℝ} (hT : 0 < T) (hab : a < b) (hD : 0 < D) (u : ℝ × ℝ → ℝ) (hu_cont : ContinuousOn u (ClosedCylinder T a b)) (t₀ x₀ : ℝ) (ht₀ : 0 < t₀) (ht₀T : t₀ ≤ T) (hx₀a : a < x₀) (hx₀b : x₀ < b) (hmax : ∀ q ∈ ClosedCylinder T a b, u q ≤ u (t₀, x₀)) : HeatOp u D (t₀, x₀) ≥ 0

Combining the time and spatial derivative tests: at an interior maximum point of $u$, the heat operator is nonnegative, $L_D u(t_0, x_0) = u_t - D u_{xx} \ge 0$ (when $D > 0$).

theorem WeakMaximumPrinciple.HeatOp_sub_eps_time (w : ℝ × ℝ → ℝ) (D ε : ℝ) (p : ℝ × ℝ) (hw_t : DifferentiableAt ℝ (fun (t : ℝ) => w (t, p.2)) p.1) : HeatOp (fun (q : ℝ × ℝ) => w q - ε * q.1) D p = HeatOp w D p - ε

The perturbation identity: $L_D(w - \varepsilon t) = L_D w - \varepsilon$, used to convert a non-strict inequality $L_D w \le 0$ into a strict one for the perturbed function.

theorem WeakMaximumPrinciple.HeatOp_sub (w v : ℝ × ℝ → ℝ) (hw : ContDiff ℝ 2 w) (hv : ContDiff ℝ 2 v) (D : ℝ) (p : ℝ × ℝ) : HeatOp (fun (q : ℝ × ℝ) => w q - v q) D p = HeatOp w D p - HeatOp v D p

Linearity of the heat operator under subtraction: $L_D(w - v) = L_D w - L_D v$ for $C^2$ functions $w$ and $v$.

theorem WeakMaximumPrinciple.HeatOp_sub_time_const (u : ℝ × ℝ → ℝ) (hu : ContDiff ℝ 2 u) (D M : ℝ) (p : ℝ × ℝ) : HeatOp (fun (q : ℝ × ℝ) => u q - q.1 * M) D p = HeatOp u D p - M

Perturbation by a linear-in-time term: $L_D(u - tM) = L_D u - M$, used in the stability estimate proof.

theorem WeakMaximumPrinciple.strict_max_on_ParabolicBoundary {T a b D : ℝ} (hT : 0 < T) (hab : a < b) (hD : 0 < D) (u : ℝ × ℝ → ℝ) (hu_cont : ContinuousOn u (ClosedCylinder T a b)) (hL_neg : ∀ (t x : ℝ), 0 < t → t ≤ T → a < x → x < b → HeatOp u D (t, x) < 0) (p : ℝ × ℝ) : p ∈ ClosedCylinder T a b → u p ≤ sSup (u '' ParabolicBoundary T a b)

Strict version of the weak maximum principle: if $L_D u < 0$ strictly throughout the interior of $Q_T$, then $u$ attains its maximum on the closed cylinder on the parabolic boundary $\partial_p Q_T$.

theorem WeakMaximumPrinciple.weak_maximum_principle {T a b D : ℝ} (hT : 0 < T) (hab : a < b) (hD : 0 < D) (w : ℝ × ℝ → ℝ) (hw_smooth : ContDiffOn ℝ 2 w (SpacetimeCylinder T a b)) (hw_cont : ContinuousOn w (ClosedCylinder T a b)) (hL : ∀ (t x : ℝ), 0 < t → t ≤ T → a < x → x < b → HeatOp w D (t, x) ≤ 0) (hw_diff_t : ∀ (t x : ℝ), 0 < t → t ≤ T → a < x → x < b → DifferentiableAt ℝ (fun (t' : ℝ) => w (t', x)) t) (p : ℝ × ℝ) : p ∈ ClosedCylinder T a b → w p ≤ sSup (w '' ParabolicBoundary T a b)

Theorem 1.1 (Weak Maximum Principle). Let $w \in C^2(Q_T) \cap C(\overline{Q_T})$ be a solution to the heat equation $w_t - D \Delta w = f$ with $f \le 0$. Then $w$ attains its maximum on $\overline{Q_T}$ on the parabolic boundary $\partial_p Q_T$, i.e. $w(p) \le \sup_{\partial_p Q_T} w$ for every $p \in \overline{Q_T}$.

theorem WeakMaximumPrinciple.comparison_principle {T a b D : ℝ} (hT : 0 < T) (hab : a < b) (hD : 0 < D) (v w : ℝ × ℝ → ℝ) (hv_smooth : ContDiff ℝ 2 v) (hw_smooth : ContDiff ℝ 2 w) (hv_cont : ContinuousOn v (ClosedCylinder T a b)) (hw_cont : ContinuousOn w (ClosedCylinder T a b)) (hfg : ∀ (t x : ℝ), 0 < t → t ≤ T → a < x → x < b → HeatOp v D (t, x) ≥ HeatOp w D (t, x)) (hbdry : ∀ p ∈ ParabolicBoundary T a b, v p ≥ w p) (p : ℝ × ℝ) : p ∈ ClosedCylinder T a b → v p ≥ w p

Comparison principle. If $v, w$ are $C^2$ functions on the closed cylinder with $L_D v \ge L_D w$ in the interior and $v \ge w$ on the parabolic boundary, then $v \ge w$ on all of $\overline{Q_T}$.

theorem WeakMaximumPrinciple.stability_estimate {T a b D : ℝ} (hT : 0 < T) (hab : a < b) (hD : 0 < D) (v w : ℝ × ℝ → ℝ) (hv_smooth : ContDiff ℝ 2 v) (hw_smooth : ContDiff ℝ 2 w) (hv_cont : ContinuousOn v (ClosedCylinder T a b)) (hw_cont : ContinuousOn w (ClosedCylinder T a b)) (M : ℝ) (hM_nonneg : 0 ≤ M) (hM : ∀ p ∈ ClosedCylinder T a b, |HeatOp w D p - HeatOp v D p| ≤ M) (p : ℝ × ℝ) : p ∈ ClosedCylinder T a b → |v p - w p| ≤ sSup ((fun (q : ℝ × ℝ) => |v q - w q|) '' ParabolicBoundary T a b) + T * M

Stability estimate. If $|L_D w - L_D v| \le M$ on $\overline{Q_T}$, then $\max_{\overline{Q_T}} |v - w| \le \max_{\partial_p Q_T} |v - w| + T \cdot M$, giving stability of the solution with respect to the right-hand side.

theorem WeakMaximumPrinciple.corollary_1_0_1 {T a b D : ℝ} (hT : 0 < T) (hab : a < b) (hD : 0 < D) (v w : ℝ × ℝ → ℝ) (hv_smooth : ContDiff ℝ 2 v) (hw_smooth : ContDiff ℝ 2 w) (hv_cont : ContinuousOn v (ClosedCylinder T a b)) (hw_cont : ContinuousOn w (ClosedCylinder T a b)) (hfg : ∀ (t x : ℝ), 0 < t → t ≤ T → a < x → x < b → HeatOp v D (t, x) ≥ HeatOp w D (t, x)) (hbdry : ∀ p ∈ ParabolicBoundary T a b, v p ≥ w p) (M : ℝ) (hM_nonneg : 0 ≤ M) (hM : ∀ p ∈ ClosedCylinder T a b, |HeatOp w D p - HeatOp v D p| ≤ M) : (∀ p ∈ ClosedCylinder T a b, v p ≥ w p) ∧ ∀ p ∈ ClosedCylinder T a b, |v p - w p| ≤ sSup ((fun (q : ℝ × ℝ) => |v q - w q|) '' ParabolicBoundary T a b) + T * M

Corollary 1.0.1 (Comparison Principle and Stability). Combines the comparison principle and the stability estimate: under appropriate $C^2$ regularity hypotheses, if $L_D v \ge L_D w$ and $v \ge w$ on $\partial_p Q_T$, then $v \ge w$ throughout $\overline{Q_T}$; and if $|L_D w - L_D v| \le M$ on $\overline{Q_T}$, then $\max_{\overline{Q_T}} |v - w| \le \max_{\partial_p Q_T} |v - w| + T \cdot M$.