The maximum principle for Δ + b·∇ (a first-order drift term) #
TauCeti.Analysis.InnerProductSpace.Laplacian.WeakMaximumPrinciple proves the maximum
principle for the bare Laplacian Δ (subharmonic functions), and
TauCeti.Analysis.InnerProductSpace.Laplacian.ZerothOrderMaximumPrinciple adds a
zeroth-order term c. This file supplies the missing first-order (transport/advection)
term: the maximum principle for the second-order elliptic operator
L u = Δ u + ⟪b, ∇u⟫
with a bounded drift field b : E → E. In Lean the directional derivative ⟪b x, ∇u x⟫
is spelled fderiv ℝ u x (b x), so the operator value at x is Δ u x + fderiv ℝ u x (b x).
The two ingredients, both classical:
- The strict principle needs no hypothesis on
b. At an interior local maximum the gradient vanishes (IsLocalMax.fderiv_eq_zero), so the drift termfderiv ℝ u x (b x)drops out and onlyΔ u x ≤ 0survives; a strict sign0 < Δ u x + fderiv ℝ u x (b x)is therefore impossible there. This isnot_isLocalMax_of_laplacian_add_fderiv_pos. - The weak principle needs a bounded drift
‖b x‖ ≤ β. Perturbing by the barrierw = exp (α ⟪u, ·⟫)for a unit vectoruandα = β + 1givesΔ w + ⟪b, ∇w⟫ = α (α + ⟪u, b⟫) w > 0, because⟪u, b x⟫ ≥ -‖b x‖ ≥ -β; letting the perturbation vanish recovers the borderline0 ≤ Δ u + fderiv ℝ u (b)case.
The exponential-barrier argument follows the weak maximum principle proof in Gilbarg--Trudinger, Elliptic Partial Differential Equations of Second Order, Chapter 3.
Main declarations #
TauCeti.laplacian_exp_inner:Δ (exp (α ⟪u, ·⟫)) x = α² ‖u‖² exp (α ⟪u, x⟫), the exponential barrier's Laplacian.TauCeti.fderiv_exp_inner_apply: the directional derivative of the same barrier.TauCeti.not_isLocalMax_of_laplacian_add_fderiv_pos/TauCeti.not_isLocalMin_of_laplacian_add_fderiv_neg: a strict sign ofΔ u + ⟪b, ∇u⟫forbids an interior local extremum, with no hypothesis onb.TauCeti.exists_mem_frontier_isMaxOn_of_laplacian_add_fderiv_pos/TauCeti.exists_mem_frontier_isMinOn_of_laplacian_add_fderiv_neg: strict boundary extremum principles.TauCeti.le_of_laplacian_add_fderiv_nonneg_le_frontier/TauCeti.ge_of_laplacian_add_fderiv_nonpos_ge_frontier: the weak maximum principle forΔ + b·∇with bounded drift, in bound form.TauCeti.exists_mem_frontier_isMaxOn_of_laplacian_add_fderiv_nonneg/TauCeti.exists_mem_frontier_isMinOn_of_laplacian_add_fderiv_nonpos: the∃-form of the weak principle.
The exponential barrier y ↦ exp (α ⟪u, y⟫) is smooth, being the exponential of a continuous
linear form.
The directional derivative of the exponential barrier y ↦ exp (α ⟪u, y⟫).
The Laplacian of the exponential barrier. For a fixed vector u, the function
y ↦ exp (α ⟪u, y⟫) has Laplacian α² ‖u‖² exp (α ⟪u, y⟫), because it is an exponential of
a linear form: the second directional derivative along an orthonormal basis vector eᵢ
contributes α² ⟪u, eᵢ⟫², and these sum to α² ‖u‖². This is the barrier for the weak
maximum principle with drift.
Strict interior obstruction. If 0 < Δ f x + fderiv ℝ f x v at a point where f is
C², then f has no local maximum at x. The direction v is arbitrary: at a local
maximum the derivative fderiv ℝ f x vanishes, so the first-order term contributes nothing
and only the Laplacian's nonpositivity survives.
Strict interior obstruction, minimum form. If Δ f x + fderiv ℝ f x v < 0 at a point
where f is C², then f has no local minimum at x.
Strict boundary maximum principle for Δ + b·∇. Let K be compact and nonempty. If
f is continuous on K, is C² on interior K, and satisfies
0 < Δ f x + fderiv ℝ f x (b x) throughout interior K, then some maximum point of f on
K lies on frontier K. No hypothesis on the drift field b is needed.
Strict boundary minimum principle for Δ + b·∇. The dual of
exists_mem_frontier_isMaxOn_of_laplacian_add_fderiv_pos.
The normalized exponential barrier for a drift bounded by β is a strict subsolution of
Δ + b·∇.
The operator Δ + b·∇ is linear under addition of a constant multiple.
Weak maximum principle for Δ + b·∇ with bounded drift.
Let K be compact. If f is continuous on K, is C² on interior K, the drift field is
bounded there (‖b x‖ ≤ β), and 0 ≤ Δ f x + fderiv ℝ f x (b x) (a subsolution of
Δ + b·∇), then any bound m that f respects on frontier K bounds f on all of K.
Weak minimum principle for Δ + b·∇ with bounded drift. The dual of
le_of_laplacian_add_fderiv_nonneg_le_frontier for supersolutions
(Δ f x + fderiv ℝ f x (b x) ≤ 0).
Comparison principle for Δ + b·∇. Two functions acted on by the same bounded drift
are ordered on a compact set if their operator values and frontier values are ordered.
Uniqueness principle for Δ + b·∇. Functions with equal operator values for the same
bounded drift and equal frontier data agree throughout the compact set.
The ∃-form of the weak maximum principle for Δ + b·∇: a subsolution with bounded drift
on a nonempty compact set attains a maximum on the frontier.
The ∃-form of the weak minimum principle for Δ + b·∇: a supersolution with bounded
drift on a nonempty compact set attains a minimum on the frontier.