Hopf's boundary-point lemma #
The weak maximum principles of TauCeti.Analysis.InnerProductSpace.Laplacian.WeakMaximumPrinciple
and TauCeti.Analysis.InnerProductSpace.Laplacian.LowerOrderMaximumPrinciple bound a subsolution
on a compact set by its frontier values; with a zeroth-order term c ≥ 0, by a nonnegative upper
bound of its frontier values. This file proves the complementary local statement at a
point where such a bound is attained: Hopf's boundary-point lemma, for the operator
-Δ - b·∇ + c with bounded drift b and bounded nonnegative zeroth-order coefficient c, and in
particular for the Laplacian.
Let B = ball y R be a ball, let e be a unit vector, and let x₀ = y + R • e be the point
where the outward ray in direction e meets the sphere ∂B. If u is continuous on
closedBall y R, twice continuously differentiable on B, and differentiable at x₀, satisfies
c u ≤ Δ u + ⟪b, ∇u⟫ on B with ‖b‖ ≤ β and 0 ≤ c ≤ γ, is nonnegative at x₀, and stays
strictly below the value u x₀ inside B while staying weakly below it on ∂B, then u leaves
x₀ in the direction e at a strictly positive rate 0 < fderiv ℝ u x₀ e. The sign condition
0 ≤ u x₀ is the usual one for a zeroth-order term; for the Laplacian (b = 0, c = 0) it is
removed by subtracting a constant, and the classical form of the lemma, in which u x₀ is a strict
maximum over the whole closed ball, follows as a corollary.
The strict inequality inside the ball is what the lemma consumes: the sphere touching at x₀
forces a one-sided bound on the derivative. The proof is the classical barrier argument. On the
closed annulus R / 2 ≤ ‖x - y‖ ≤ R one perturbs u by a positive multiple of the radial
barrier w x = ‖x - y‖ ^ p - R ^ p with p < 0, which vanishes on the outer sphere — so the
perturbation still respects the maximum bound there — and is bounded above on the inner sphere,
where the strict inequality of the hypothesis leaves a margin. With r = ‖x - y‖,
Δ w + ⟪b, ∇w⟫ = p r ^ (p - 2) (p + dim E - 2 + ⟪x - y, b⟫),
so the choice p = -(dim E + β R + γ R²) makes w a subsolution, c w ≤ Δ w + ⟪b, ∇w⟫, on the
annulus, and the weak maximum principle for -Δ - b·∇ + c applies to the perturbation. Letting
the inward ray parameter tend to zero and differentiating the resulting one-sided bound at x₀
gives the claim.
Main declarations #
TauCeti.fderiv_pos_of_mul_le_laplacian_add_fderiv_of_lt_ball_of_le_sphere: Hopf's boundary-point lemma for-Δ - b·∇ + c.TauCeti.fderiv_neg_of_laplacian_add_fderiv_le_mul_of_gt_ball_of_ge_sphere: its minimum form, for supersolutions.TauCeti.fderiv_pos_of_laplacian_nonneg_of_lt_ball_of_le_sphere: Hopf's lemma for subharmonic functions, with a strict bound in the ball and a weak bound on the sphere.TauCeti.fderiv_pos_of_laplacian_nonneg_of_lt_closedBall: the classical form of the lemma, in which the value at the boundary point is a strict maximum over the closed ball.TauCeti.fderiv_neg_of_laplacian_nonpos_of_gt_ball_of_ge_sphere: the minimum form with a weak inequality on the sphere.TauCeti.fderiv_neg_of_laplacian_nonpos_of_gt_closedBall: the superharmonic mirror image, for a strict minimum.TauCeti.fderiv_pos_of_harmonicOnNhd_of_lt_closedBall: the harmonic case of the lemma.TauCeti.fderiv_neg_of_harmonicOnNhd_of_gt_closedBall: the harmonic minimum form.
References #
L. C. Evans, Partial Differential Equations, 2nd ed., Section 6.4.2 (Hopf's lemma); D. Gilbarg and N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, Lemma 3.4.
Hopf's boundary-point lemma for -Δ - b·∇ + c. Let B = ball y R be a ball in a
finite-dimensional real inner product space, let e be a unit vector, and let x₀ = y + R • e be
the point where the outward ray in direction e meets the sphere ∂B. Let the drift satisfy
‖b‖ ≤ β and the zeroth-order coefficient 0 ≤ c ≤ γ on B. If u is continuous on
closedBall y R, twice continuously differentiable on B, and differentiable at x₀, is a
subsolution c u ≤ Δ u + ⟪b, ∇u⟫ on B, is nonnegative at x₀, and stays strictly below the
value u x₀ inside B and weakly below it on the sphere ∂B, then u leaves x₀ in the
direction e at a strictly positive rate: 0 < fderiv ℝ u x₀ e.
The sign condition 0 ≤ u x₀ is needed only because of c; for c = 0 it can be arranged by
subtracting the constant u x₀, as in
TauCeti.fderiv_pos_of_laplacian_nonneg_of_lt_ball_of_le_sphere.
Hopf's boundary-point lemma for -Δ - b·∇ + c, minimum form. The mirror image of
TauCeti.fderiv_pos_of_mul_le_laplacian_add_fderiv_of_lt_ball_of_le_sphere for supersolutions
Δ u + ⟪b, ∇u⟫ ≤ c u that are nonpositive at x₀ = y + R • e, strictly above u x₀ in the ball
and weakly above it on the sphere: the outward derivative at x₀ is negative.
Hopf's boundary-point lemma. Let B = ball y R be a ball in a finite-dimensional real
inner product space, let e be a unit vector, and let x₀ = y + R • e be the point where the
outward ray in direction e meets the sphere ∂B. If u is continuous on closedBall y R, twice
continuously differentiable on B, and differentiable at x₀, is subharmonic on B (0 ≤ Δ u),
stays strictly below the value u x₀
inside B and weakly below it on the sphere ∂B, then u leaves x₀ in the direction e at a
strictly positive rate: 0 < fderiv ℝ u x₀ e.
The strict inequality is needed only inside the ball, so the theorem applies directly when the
boundary sphere has merely a weak bound. The classical form, with a strict maximum over the whole
closed ball, is TauCeti.fderiv_pos_of_laplacian_nonneg_of_lt_closedBall.
Hopf's boundary-point lemma, classical form. The statement usually quoted, in which u
stays strictly below u x₀ at every other point of the closed ball. It is the specialization of
the ball-and-sphere form in which the strict inequality on the ball follows from the strict
closed-ball maximum and the sphere has the corresponding weak inequality.
Hopf's boundary-point lemma, minimum form. If u is continuous on closedBall y R,
twice continuously differentiable on ball y R, and differentiable at x₀, satisfies
Δ u ≤ 0 on the ball, has a strict minimum at x₀ in the ball, and has a weak minimum on the
sphere, then its derivative in the outward normal direction is negative.
Hopf's boundary-point lemma, minimum form. The mirror image of
TauCeti.fderiv_pos_of_laplacian_nonneg_of_lt_closedBall for superharmonic functions, with a
strict minimum at x₀ = y + R • e over the closed ball.
Hopf's boundary-point lemma for harmonic functions. A harmonic function on the ball whose
value at the boundary point x₀ = y + R • e is a strict maximum over closedBall y R has
strictly positive outgoing derivative there. This is the form of the lemma used to prove the
strong maximum principle and boundary-point regularity.
Hopf's boundary-point lemma for harmonic functions, minimum form. A harmonic function on
the ball whose value at the boundary point x₀ = y + R • e is a strict minimum on closedBall y R
has a strictly negative outgoing derivative there.