The strong maximum principle #
The weak maximum principles of TauCeti.Analysis.InnerProductSpace.Laplacian.WeakMaximumPrinciple
and TauCeti.Analysis.InnerProductSpace.Laplacian.LowerOrderMaximumPrinciple bound a subsolution
by its frontier values; with a zeroth-order term c ≥ 0, by a nonnegative upper bound of its
frontier values. This file proves the strong maximum principle in a finite-dimensional
real inner product space, first for the operator -Δ - b·∇ + c with locally bounded drift b and
locally bounded zeroth-order coefficient c ≥ 0, and then for the Laplacian: a C² subsolution
c u ≤ Δ u + ⟪b, ∇u⟫ on a preconnected open set that attains a nonnegative maximum over the set at
some point of it is constant there. For the Laplacian the sign condition disappears, since a
constant may be subtracted. The minimum principles, the strong comparison principles, and the
harmonic specializations follow.
The proof is the classical one via Hopf's boundary-point lemma
(TauCeti.fderiv_pos_of_mul_le_laplacian_add_fderiv_of_lt_ball_of_le_sphere), and needs neither a
mean-value property nor analyticity, so it works in every dimension and for variable lower-order
coefficients. The local step is
TauCeti.eventually_eq_of_mul_le_laplacian_add_fderiv_of_isLocalMax: near a local maximum x, if
u took a smaller value at some point x₂, then the largest ball about x₂ on which u < u x
touches the level set {u = u x} at a point x₀ of its sphere. There u is strictly below
u x₀ inside the ball and weakly below it on the sphere, so Hopf's lemma makes the outward
derivative at x₀ strictly positive; but x₀ is again a local maximum, where the derivative
vanishes. Hence u is locally constant near every point where it attains its maximum, and
preconnectedness spreads this over the whole set.
Unlike the planar statements of TauCeti.Analysis.PDE.Harnack.StrongPrinciple, which use the
analyticity of planar harmonic functions, the results here need the set to be open: a subharmonic
function may be constant near a local maximum and increase further away.
Main declarations #
TauCeti.eventually_eq_of_mul_le_laplacian_add_fderiv_of_isLocalMax: aC²subsolution of-Δ - b·∇ + cwith a nonnegative local maximum is constant near it; its supersolution mirror image isTauCeti.eventually_eq_of_laplacian_add_fderiv_le_mul_of_isLocalMin.TauCeti.eqOn_const_of_mul_le_laplacian_add_fderiv_of_isMaxOn: the strong maximum principle for-Δ - b·∇ + con a preconnected open set.TauCeti.eqOn_const_of_laplacian_add_fderiv_le_mul_of_isMinOn: the strong minimum principle for supersolutions of-Δ - b·∇ + c.TauCeti.eqOn_of_laplacian_add_fderiv_sub_mul_le_of_le_of_eq: the strong comparison principle for-Δ - b·∇ + c, which needs no sign condition onc,uorv.TauCeti.eventually_eq_of_laplacian_nonneg_of_isLocalMax: a function that isC²at a local maximum point and subharmonic near it is constant near it; its superharmonic mirror image isTauCeti.eventually_eq_of_laplacian_nonpos_of_isLocalMin.TauCeti.eqOn_const_of_laplacian_nonneg_of_isMaxOn: the strong maximum principle for subharmonic functions on a preconnected open set.TauCeti.eqOn_const_of_laplacian_nonpos_of_isMinOn: the strong minimum principle for superharmonic functions.TauCeti.eqOn_of_laplacian_le_of_le_of_eq: the strong comparison principle for the Laplacian.TauCeti.eqOn_const_closure_of_laplacian_nonneg_of_isMaxOn,TauCeti.eqOn_const_closure_of_laplacian_nonpos_of_isMinOn,TauCeti.eqOn_closure_of_laplacian_le_of_le_of_eq: the same three statements for functions continuous up to the boundary, extremal (respectively dominated) overclosure Uat a point ofU.TauCeti.eqOn_const_of_harmonicOnNhd_of_isMaxOn_of_isOpen,TauCeti.eqOn_const_of_harmonicOnNhd_of_isMinOn_of_isOpen,TauCeti.eqOn_of_harmonicOnNhd_of_le_of_eq_of_isOpen,TauCeti.eq_zero_on_of_harmonicOnNhd_of_nonneg_of_eq_zero_of_isOpen,TauCeti.eq_zero_on_or_pos_on_of_harmonicOnNhd_of_nonneg: the harmonic specializations.
References #
D. Gilbarg and N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, Theorem 3.5; L. C. Evans, Partial Differential Equations, 2nd ed., Section 6.4.2.
Local strong maximum principle for -Δ - b·∇ + c. Let u be C² at a local maximum
point x with 0 ≤ u x, and near x let u be a subsolution c u ≤ Δ u + ⟪b, ∇u⟫ with
coefficients bounded as ‖b‖ ≤ β and 0 ≤ c ≤ γ. Then u is constant on a neighbourhood of
x.
Local strong minimum principle for -Δ - b·∇ + c. A C² supersolution
Δ u + ⟪b, ∇u⟫ ≤ c u near a local minimum point x with u x ≤ 0, whose coefficients are bounded
as ‖b‖ ≤ β and 0 ≤ c ≤ γ near x, is constant on a neighbourhood of x.
Strong maximum principle for -Δ - b·∇ + c. Let U be a preconnected open set, and let
b and c ≥ 0 be locally bounded on U. A function that is C² on U, is a subsolution
c u ≤ Δ u + ⟪b, ∇u⟫ there, and attains a nonnegative maximum over U at a point a ∈ U, is
constant on U.
The sign condition 0 ≤ u a is needed only because of c: for c = 0 it can be arranged by
subtracting a constant.
Strong minimum principle for -Δ - b·∇ + c. Let U be a preconnected open set, and let
b and c ≥ 0 be locally bounded on U. A function that is C² on U, is a supersolution
Δ u + ⟪b, ∇u⟫ ≤ c u there, and attains a nonpositive minimum over U at a point a ∈ U, is
constant on U.
Strong comparison principle for -Δ - b·∇ + c. Let U be a preconnected open set, let
b be locally bounded and c locally bounded above on U, and let u and v be C² on U
with Δ v + ⟪b, ∇v⟫ - c v ≤ Δ u + ⟪b, ∇u⟫ - c u there. If u ≤ v on U and they agree at a
point of U, then they agree on all of U. No sign condition on c, u or v is needed: since
u - v ≤ 0, the difference is a subsolution for the coefficient max c 0.
Local strong maximum principle. A function that is C² at a local maximum point x and
subharmonic (0 ≤ Δ u) near x is constant on a neighbourhood of x.
Local strong minimum principle. A function that is C² at a local minimum point x and
superharmonic (Δ u ≤ 0) near x is constant on a neighbourhood of x.
Strong maximum principle for subharmonic functions. A function that is C² and
subharmonic (0 ≤ Δ u) on a preconnected open set U, and attains its maximum over U at a
point a ∈ U, is constant on U.
Strong minimum principle for superharmonic functions. A function that is C² and
superharmonic (Δ u ≤ 0) on a preconnected open set U, and attains its minimum over U at a
point a ∈ U, is constant on U.
Strong comparison principle for the Laplacian. Let u and v be C² on a preconnected
open set U, with u at least as subharmonic as v there (Δ v ≤ Δ u). If u ≤ v on U and
they agree at a point of U, then they agree on all of U.
Strong maximum principle up to the boundary. If u is continuous on closure U, is C²
and subharmonic on the preconnected open set U, and attains its maximum over closure U at a
point a ∈ U, then u is constant on closure U.
Strong minimum principle up to the boundary. If u is continuous on closure U, is C²
and superharmonic on the preconnected open set U, and attains its minimum over closure U at a
point a ∈ U, then u is constant on closure U.
Strong comparison principle up to the boundary. Let u and v be continuous on
closure U and C² on the preconnected open set U, with Δ v ≤ Δ u on U. If u ≤ v on
closure U and they agree at a point of U, then they agree on all of closure U.
Strong maximum principle for harmonic functions. A real-valued harmonic function on a preconnected open set that attains its maximum over the set at one of its points is constant there.
Strong minimum principle for harmonic functions. A real-valued harmonic function on a preconnected open set that attains its minimum over the set at one of its points is constant there.
Strong comparison principle for harmonic functions. Two harmonic functions on a preconnected open set, one below the other, that agree at one point of the set agree throughout it.
A nonnegative harmonic function on a preconnected open set that vanishes at one point of the set vanishes throughout it.
A nonnegative harmonic function on a preconnected open set either vanishes identically or is strictly positive everywhere on the set.