Corollaries of Hopf's lemma and the strong maximum principle

The free-sign clauses of Hopf's lemma and of the strong maximum principle, in which the zeroth-order coefficient has any sign and the extremal value is zero, follow from the nonnegative clauses by replacing c with its positive part: on the set where the function is nonpositive the change of coefficient lowers the operator. The avoidance principle, the tangency corollary at a boundary point with an interior sphere, and uniqueness for the Neumann problem up to a constant then follow.

Main declarations

• EllipticPdes.Classical.hopf_lemma_of_zero: Hopf's lemma with c of any sign and u x₀ = 0.
• EllipticPdes.Classical.strong_maximum_principle_of_zero: the strong principle at a zero maximum with c of any sign.
• EllipticPdes.Classical.avoidance_principle: two ordered functions with ordered images either agree or are strictly ordered.
• EllipticPdes.Classical.eq_of_eq_of_fderiv_eq: tangency at a boundary point with an interior sphere forces equality.
• EllipticPdes.Classical.neumann_unique: uniqueness up to a constant for the Neumann problem.

Operator convention

The non-divergence operator here is L u = -∑ aᵢⱼ ∂ᵢⱼu + ∑ bᵢ ∂ᵢu + c u. All Guo results cited in this file are translated by negating the source operator: Guo's operator is -L, with coefficients a, -b, -c. Thus his subsolution inequality (-L) u ≥ 0 becomes L u ≤ 0, and his potential condition -c ≤ 0 becomes c ≥ 0.

References

James Guo, Partial Differential Equations (Course Lecture Notes), Lemma XI.4.3, Theorem XI.4.5, Corollaries XI.4.6, XI.4.7 and XI.4.8 (pp. 100–103).

theorem EllipticPdes.Classical.nondivOp_posPart_le {d : ℕ} (a : EuclideanSpace ℝ (Fin d) → Fin d → Fin d → ℝ) (b : EuclideanSpace ℝ (Fin d) → Fin d → ℝ) (c : EuclideanSpace ℝ (Fin d) → ℝ) {u : EuclideanSpace ℝ (Fin d) → ℝ} {x : EuclideanSpace ℝ (Fin d)} (hux : u x ≤ 0) : nondivOp a b (fun (y : EuclideanSpace ℝ (Fin d)) => max (c y) 0) u x ≤ nondivOp a b c u x

The operator with the positive part of the zeroth-order coefficient is at most the operator with the coefficient itself, on a nonpositive function.

theorem EllipticPdes.Classical.hopf_lemma_of_zero {d : ℕ} (hd : 0 < d) {U : Set (EuclideanSpace ℝ (Fin d))} {a : EuclideanSpace ℝ (Fin d) → Fin d → Fin d → ℝ} {b : EuclideanSpace ℝ (Fin d) → Fin d → ℝ} {θ A B : ℝ} (hθ : 0 < θ) (hsymm : ∀ x ∈ U, ∀ (i j : Fin d), a x i j = a x j i) (hell : ∀ x ∈ U, ∀ (ξ : Fin d → ℝ), θ * ∑ i : Fin d, ξ i ^ 2 ≤ ∑ i : Fin d, ∑ j : Fin d, a x i j * ξ i * ξ j) (ha : ∀ x ∈ U, ∀ (i j : Fin d), |a x i j| ≤ A) (hb : ∀ x ∈ U, ∀ (i : Fin d), |b x i| ≤ B) {c : EuclideanSpace ℝ (Fin d) → ℝ} {C : ℝ} (hc : ∀ x ∈ U, |c x| ≤ C) {u : EuclideanSpace ℝ (Fin d) → ℝ} (hu : ContDiffOn ℝ 2 u U) (huc : ContinuousOn u (closure U)) (hsub : ∀ x ∈ U, nondivOp a b c u x ≤ 0) {x₀ y : EuclideanSpace ℝ (Fin d)} {r : ℝ} (hr : 0 < r) (hball : Metric.ball y r ⊆ U) (hx₀ : dist x₀ y = r) (hlt : ∀ x ∈ U, u x < u x₀) (hu0 : u x₀ = 0) (hdiff : DifferentiableAt ℝ u x₀) : 0 < (fderiv ℝ u x₀) (x₀ - y)

Hopf's lemma at a zero boundary value (Guo Lemma XI.4.3(iii)). With the zeroth-order coefficient bounded in absolute value and of any sign, a subsolution strictly negative on the ball, vanishing at a point x₀ of the sphere and differentiable there, has positive derivative at x₀ in the outward radial direction.

theorem EllipticPdes.Classical.strong_maximum_principle_of_zero {d : ℕ} (hd : 0 < d) {U : Set (EuclideanSpace ℝ (Fin d))} (hU : IsOpen U) (hUc : IsPreconnected U) {a : EuclideanSpace ℝ (Fin d) → Fin d → Fin d → ℝ} {b : EuclideanSpace ℝ (Fin d) → Fin d → ℝ} {θ A B : ℝ} (hθ : 0 < θ) (hsymm : ∀ x ∈ U, ∀ (i j : Fin d), a x i j = a x j i) (hell : ∀ x ∈ U, ∀ (ξ : Fin d → ℝ), θ * ∑ i : Fin d, ξ i ^ 2 ≤ ∑ i : Fin d, ∑ j : Fin d, a x i j * ξ i * ξ j) (ha : ∀ x ∈ U, ∀ (i j : Fin d), |a x i j| ≤ A) (hb : ∀ x ∈ U, ∀ (i : Fin d), |b x i| ≤ B) {c : EuclideanSpace ℝ (Fin d) → ℝ} {C : ℝ} (hc : ∀ x ∈ U, |c x| ≤ C) {u : EuclideanSpace ℝ (Fin d) → ℝ} (hu : ContDiffOn ℝ 2 u U) (hsub : ∀ x ∈ U, nondivOp a b c u x ≤ 0) {x₀ : EuclideanSpace ℝ (Fin d)} (hx₀ : x₀ ∈ U) (hmax : ∀ x ∈ U, u x ≤ u x₀) (hu0 : u x₀ = 0) (x : EuclideanSpace ℝ (Fin d)) : x ∈ U → u x = u x₀

Strong maximum principle at a zero maximum (Guo Theorem XI.4.5(iii)). With the zeroth-order coefficient bounded in absolute value and of any sign, a subsolution on a connected open set that attains the maximum zero at an interior point vanishes on the set.

theorem EllipticPdes.Classical.avoidance_principle {d : ℕ} (hd : 0 < d) {U : Set (EuclideanSpace ℝ (Fin d))} (hU : IsOpen U) (hUc : IsPreconnected U) {a : EuclideanSpace ℝ (Fin d) → Fin d → Fin d → ℝ} {b : EuclideanSpace ℝ (Fin d) → Fin d → ℝ} {θ A B : ℝ} (hθ : 0 < θ) (hsymm : ∀ x ∈ U, ∀ (i j : Fin d), a x i j = a x j i) (hell : ∀ x ∈ U, ∀ (ξ : Fin d → ℝ), θ * ∑ i : Fin d, ξ i ^ 2 ≤ ∑ i : Fin d, ∑ j : Fin d, a x i j * ξ i * ξ j) (ha : ∀ x ∈ U, ∀ (i j : Fin d), |a x i j| ≤ A) (hb : ∀ x ∈ U, ∀ (i : Fin d), |b x i| ≤ B) {c : EuclideanSpace ℝ (Fin d) → ℝ} {C : ℝ} (hc : ∀ x ∈ U, |c x| ≤ C) {u v : EuclideanSpace ℝ (Fin d) → ℝ} (hu : ContDiffOn ℝ 2 u U) (hv : ContDiffOn ℝ 2 v U) (hL : ∀ x ∈ U, nondivOp a b c u x ≤ nondivOp a b c v x) (hle : ∀ x ∈ U, u x ≤ v x) : (∀ x ∈ U, u x = v x) ∨ ∀ x ∈ U, u x < v x

Avoidance principle (Guo Corollary XI.4.6). On a connected open set, with the zeroth-order coefficient bounded in absolute value, two functions with L u ≤ L v and u ≤ v either agree everywhere or satisfy u < v everywhere.

theorem EllipticPdes.Classical.eq_of_eq_of_fderiv_eq {d : ℕ} (hd : 0 < d) {U : Set (EuclideanSpace ℝ (Fin d))} (hU : IsOpen U) (hUc : IsPreconnected U) {a : EuclideanSpace ℝ (Fin d) → Fin d → Fin d → ℝ} {b : EuclideanSpace ℝ (Fin d) → Fin d → ℝ} {θ A B : ℝ} (hθ : 0 < θ) (hsymm : ∀ x ∈ U, ∀ (i j : Fin d), a x i j = a x j i) (hell : ∀ x ∈ U, ∀ (ξ : Fin d → ℝ), θ * ∑ i : Fin d, ξ i ^ 2 ≤ ∑ i : Fin d, ∑ j : Fin d, a x i j * ξ i * ξ j) (ha : ∀ x ∈ U, ∀ (i j : Fin d), |a x i j| ≤ A) (hb : ∀ x ∈ U, ∀ (i : Fin d), |b x i| ≤ B) {c : EuclideanSpace ℝ (Fin d) → ℝ} {C : ℝ} (hc : ∀ x ∈ U, |c x| ≤ C) {u v : EuclideanSpace ℝ (Fin d) → ℝ} (hu : ContDiffOn ℝ 2 u U) (hv : ContDiffOn ℝ 2 v U) (huc : ContinuousOn u (closure U)) (hvc : ContinuousOn v (closure U)) (hL : ∀ x ∈ U, nondivOp a b c u x ≤ nondivOp a b c v x) (hle : ∀ x ∈ U, u x ≤ v x) {x₀ y : EuclideanSpace ℝ (Fin d)} {r : ℝ} (hr : 0 < r) (hball : Metric.ball y r ⊆ U) (hx₀ : dist x₀ y = r) (heq : u x₀ = v x₀) (hfd : fderiv ℝ u x₀ = fderiv ℝ v x₀) (hud : DifferentiableAt ℝ u x₀) (hvd : DifferentiableAt ℝ v x₀) (x : EuclideanSpace ℝ (Fin d)) : x ∈ U → u x = v x

Tangency at a boundary point forces equality (Guo Corollary XI.4.7, with the interior sphere condition at the point in place of a C² boundary). On a connected open set, two functions with L u ≤ L v, u ≤ v on the set, equal with equal derivatives at a point x₀ of the frontier that is on the sphere of a ball inside the set, agree on the set.

theorem EllipticPdes.Classical.eq_on_closure_of_eq_on {d : ℕ} {U : Set (EuclideanSpace ℝ (Fin d))} {w : EuclideanSpace ℝ (Fin d) → ℝ} (hwc : ContinuousOn w (closure U)) {M : ℝ} (h : ∀ x ∈ U, w x = M) (x : EuclideanSpace ℝ (Fin d)) : x ∈ closure U → w x = M

A function that is constant on an open set and continuous on its closure is constant on the closure.

theorem EllipticPdes.Classical.eq_const_of_neumann_aux {d : ℕ} (hd : 0 < d) {U : Set (EuclideanSpace ℝ (Fin d))} (hU : IsOpen U) (hUc : IsPreconnected U) {a : EuclideanSpace ℝ (Fin d) → Fin d → Fin d → ℝ} {b : EuclideanSpace ℝ (Fin d) → Fin d → ℝ} {c : EuclideanSpace ℝ (Fin d) → ℝ} {θ A B C : ℝ} (hθ : 0 < θ) (hsymm : ∀ x ∈ U, ∀ (i j : Fin d), a x i j = a x j i) (hell : ∀ x ∈ U, ∀ (ξ : Fin d → ℝ), θ * ∑ i : Fin d, ξ i ^ 2 ≤ ∑ i : Fin d, ∑ j : Fin d, a x i j * ξ i * ξ j) (ha : ∀ x ∈ U, ∀ (i j : Fin d), |a x i j| ≤ A) (hb : ∀ x ∈ U, ∀ (i : Fin d), |b x i| ≤ B) (hc0 : ∀ x ∈ U, 0 ≤ c x) (hcC : ∀ x ∈ U, c x ≤ C) {w : EuclideanSpace ℝ (Fin d) → ℝ} (hw : ContDiffOn ℝ 2 w U) (hwc : ContinuousOn w (closure U)) (hsub : ∀ x ∈ U, nondivOp a b c w x ≤ 0) (hν : ∀ y ∈ frontier U, DifferentiableAt ℝ w y ∧ ∃ (z : EuclideanSpace ℝ (Fin d)) (r : ℝ), 0 < r ∧ Metric.ball z r ⊆ U ∧ dist y z = r ∧ (fderiv ℝ w y) (y - z) = 0) {p : EuclideanSpace ℝ (Fin d)} (hp : p ∈ closure U) (hpmax : ∀ x ∈ closure U, w x ≤ w p) (hp0 : 0 ≤ w p) (x : EuclideanSpace ℝ (Fin d)) : x ∈ closure U → w x = w p

A solution with nonnegative maximum over the closure and zero normal derivative along an interior sphere at every frontier point is constant on the closure.

theorem EllipticPdes.Classical.neumann_unique {d : ℕ} (hd : 0 < d) {U : Set (EuclideanSpace ℝ (Fin d))} (hU : IsOpen U) (hUc : IsPreconnected U) (hUb : Bornology.IsBounded U) (hUne : U.Nonempty) {a : EuclideanSpace ℝ (Fin d) → Fin d → Fin d → ℝ} {b : EuclideanSpace ℝ (Fin d) → Fin d → ℝ} {c : EuclideanSpace ℝ (Fin d) → ℝ} {θ A B C : ℝ} (hθ : 0 < θ) (hsymm : ∀ x ∈ U, ∀ (i j : Fin d), a x i j = a x j i) (hell : ∀ x ∈ U, ∀ (ξ : Fin d → ℝ), θ * ∑ i : Fin d, ξ i ^ 2 ≤ ∑ i : Fin d, ∑ j : Fin d, a x i j * ξ i * ξ j) (ha : ∀ x ∈ U, ∀ (i j : Fin d), |a x i j| ≤ A) (hb : ∀ x ∈ U, ∀ (i : Fin d), |b x i| ≤ B) (hc0 : ∀ x ∈ U, 0 ≤ c x) (hcC : ∀ x ∈ U, c x ≤ C) {u v : EuclideanSpace ℝ (Fin d) → ℝ} (hu : ContDiffOn ℝ 2 u U) (hv : ContDiffOn ℝ 2 v U) (huc : ContinuousOn u (closure U)) (hvc : ContinuousOn v (closure U)) (hL : ∀ x ∈ U, nondivOp a b c u x = nondivOp a b c v x) (hν : ∀ y ∈ frontier U, DifferentiableAt ℝ u y ∧ DifferentiableAt ℝ v y ∧ ∃ (z : EuclideanSpace ℝ (Fin d)) (r : ℝ), 0 < r ∧ Metric.ball z r ⊆ U ∧ dist y z = r ∧ (fderiv ℝ u y) (y - z) = (fderiv ℝ v y) (y - z)) : ∃ (M : ℝ), ∀ x ∈ closure U, u x = v x + M

Uniqueness for the Neumann problem (Guo Corollary XI.4.8). On a bounded connected open set with an interior sphere at every frontier point, with c ≥ 0 bounded, two functions with the same image under L, differentiable at every frontier point and with the same derivative there along the radius of an interior sphere, differ by a constant on the closure.

theorem EllipticPdes.Classical.neumann_unique_of_exists_pos {d : ℕ} (hd : 0 < d) {U : Set (EuclideanSpace ℝ (Fin d))} (hU : IsOpen U) (hUc : IsPreconnected U) (hUb : Bornology.IsBounded U) (hUne : U.Nonempty) {a : EuclideanSpace ℝ (Fin d) → Fin d → Fin d → ℝ} {b : EuclideanSpace ℝ (Fin d) → Fin d → ℝ} {c : EuclideanSpace ℝ (Fin d) → ℝ} {θ A B C : ℝ} (hθ : 0 < θ) (hsymm : ∀ x ∈ U, ∀ (i j : Fin d), a x i j = a x j i) (hell : ∀ x ∈ U, ∀ (ξ : Fin d → ℝ), θ * ∑ i : Fin d, ξ i ^ 2 ≤ ∑ i : Fin d, ∑ j : Fin d, a x i j * ξ i * ξ j) (ha : ∀ x ∈ U, ∀ (i j : Fin d), |a x i j| ≤ A) (hb : ∀ x ∈ U, ∀ (i : Fin d), |b x i| ≤ B) (hc0 : ∀ x ∈ U, 0 ≤ c x) (hcC : ∀ x ∈ U, c x ≤ C) (hcpos : ∃ x ∈ U, c x ≠ 0) {u v : EuclideanSpace ℝ (Fin d) → ℝ} (hu : ContDiffOn ℝ 2 u U) (hv : ContDiffOn ℝ 2 v U) (huc : ContinuousOn u (closure U)) (hvc : ContinuousOn v (closure U)) (hL : ∀ x ∈ U, nondivOp a b c u x = nondivOp a b c v x) (hν : ∀ y ∈ frontier U, DifferentiableAt ℝ u y ∧ DifferentiableAt ℝ v y ∧ ∃ (z : EuclideanSpace ℝ (Fin d)) (r : ℝ), 0 < r ∧ Metric.ball z r ⊆ U ∧ dist y z = r ∧ (fderiv ℝ u y) (y - z) = (fderiv ℝ v y) (y - z)) (x : EuclideanSpace ℝ (Fin d)) : x ∈ closure U → u x = v x

Uniqueness for the Neumann problem with a nonzero zeroth-order coefficient (Guo Remark XI.4.9). When c is positive somewhere on the set, the constant is zero.