A maximum principle for functions vanishing on the axis

lem:aniso:axis: a function φ(r, z, t) which is continuous on the closed half-disc K = {r ≥ 0, r² + z² ≤ R²} × [t₁, s], vanishes on the axis r = 0, and satisfies the parabolic equation eq:aniso:axis:pde on the open set D obeys |φ| ≤ max_Σ |φ| + M (t - t₁) on K, where Σ is the parabolic boundary and M bounds the forcing F. No bound is assumed on the drift b_r, b_z, the zeroth-order coefficient γ ≥ 0, or the singular coefficient k / r: at an interior maximum point they multiply first derivatives which vanish.

The proof is the printed one: the perturbation φ - (M + ε)(t - t₁) attains its maximum on the compact set K; the maximum point lies neither on Σ nor on the axis, so it lies in D, where the first-order spatial derivatives vanish, the second-order ones are nonpositive, and the left time derivative is nonnegative, contradicting the equation.

theorem CIV.dr_neg (φ : (ℝ × ℝ) × ℝ → ℝ) (p : (ℝ × ℝ) × ℝ) : dr (fun (q : (ℝ × ℝ) × ℝ) => -φ q) p = -dr φ p

∂_r commutes with negation.

theorem CIV.dz_neg (φ : (ℝ × ℝ) × ℝ → ℝ) (p : (ℝ × ℝ) × ℝ) : dz (fun (q : (ℝ × ℝ) × ℝ) => -φ q) p = -dz φ p

∂_z commutes with negation.

theorem CIV.dtPast_neg (φ : (ℝ × ℝ) × ℝ → ℝ) (p : (ℝ × ℝ) × ℝ) : dtPast (fun (q : (ℝ × ℝ) × ℝ) => -φ q) p = -dtPast φ p

The one-sided time derivative commutes with negation.

theorem CIV.deriv_deriv_nonpos_of_isLocalMax {f : ℝ → ℝ} {a : ℝ} (hf : ContDiffAt ℝ 2 f a) (hmax : IsLocalMax f a) : deriv (deriv f) a ≤ 0

At a local maximum of a C² function of one real variable, the second derivative is nonpositive.

theorem CIV.isCompact_axisClosedDomain (R t₁ s : ℝ) (hR : 0 < R) : IsCompact (axisClosedDomain R t₁ s)

The closed half-disc with its time interval is compact.

theorem CIV.axisMaximumPrinciple_upper (R t₁ s k M : ℝ) (hR : 0 < R) (hts : t₁ < s) (hM : 0 ≤ M) (φ br bz γ F : (ℝ × ℝ) × ℝ → ℝ) (hcont : ContinuousOn φ (axisClosedDomain R t₁ s)) (haxis : ∀ (z t : ℝ), |z| ≤ R → t₁ ≤ t → t ≤ s → φ ((0, z), t) = 0) (hreg : ∀ p ∈ axisDomain R t₁ s, ContDiffAt ℝ 2 (fun (y : ℝ × ℝ) => φ (y, p.2)) p.1 ∧ DifferentiableWithinAt ℝ (fun (t : ℝ) => φ (p.1, t)) (Set.Iic p.2) p.2) (hγ : ∀ p ∈ axisDomain R t₁ s, 0 ≤ γ p) (hF : ∀ p ∈ axisDomain R t₁ s, |F p| ≤ M) (hpde : ∀ p ∈ axisDomain R t₁ s, dtPast φ p + br p * dr φ p + bz p * dz φ p + γ p * φ p = dr (dr φ) p + k / p.1.1 * dr φ p + dz (dz φ) p + F p) (m : ℝ) (hm : ∀ p ∈ axisParabolicBoundary R t₁ s, |φ p| ≤ m) (p : (ℝ × ℝ) × ℝ) : p ∈ axisClosedDomain R t₁ s → φ p ≤ m + M * (p.2 - t₁)

The one-sided bound of lem:aniso:axis: under its hypotheses, φ ≤ max_Σ |φ| + M (t - t₁) on the closed domain.

theorem CIV.axisMaximumPrinciple_of_profile (R t₁ s k M : ℝ) (hR : 0 < R) (hts : t₁ < s) (hM : 0 ≤ M) (φ br bz γ F : (ℝ × ℝ) × ℝ → ℝ) (hcont : ContinuousOn φ (axisClosedDomain R t₁ s)) (haxis : ∀ (z t : ℝ), |z| ≤ R → t₁ ≤ t → t ≤ s → φ ((0, z), t) = 0) (hreg : ∀ p ∈ axisDomain R t₁ s, ContDiffAt ℝ 2 (fun (y : ℝ × ℝ) => φ (y, p.2)) p.1 ∧ DifferentiableWithinAt ℝ (fun (t : ℝ) => φ (p.1, t)) (Set.Iic p.2) p.2) (hγ : ∀ p ∈ axisDomain R t₁ s, 0 ≤ γ p) (hF : ∀ p ∈ axisDomain R t₁ s, |F p| ≤ M) (hpde : ∀ p ∈ axisDomain R t₁ s, dtPast φ p + br p * dr φ p + bz p * dz φ p + γ p * φ p = dr (dr φ) p + k / p.1.1 * dr φ p + dz (dz φ) p + F p) (m : ℝ) : (∀ p ∈ axisParabolicBoundary R t₁ s, |φ p| ≤ m) → ∀ p ∈ axisClosedDomain R t₁ s, |φ p| ≤ m + M * (p.2 - t₁)

lem:aniso:axis, the maximum principle for functions vanishing on the axis: if φ is continuous on the closed half-disc K = {r ≥ 0, r² + z² ≤ R²} × [t₁, s], vanishes on the axis r = 0, is C² in (r, z) and differentiable from the past in t on D, and satisfies eq:aniso:axis:pde on D with γ ≥ 0 and |F| ≤ M, then |φ| ≤ max_Σ |φ| + M (t - t₁) on K (eq:aniso:axis:bound). The maximum over the parabolic boundary Σ enters as any bound m for |φ| on Σ.