The maximizer step shared by the lower-order weak maximum principles

Both lower-order weak maximum principles — for -Δ + c in TauCeti.Analysis.InnerProductSpace.Laplacian.ZerothOrderMaximumPrinciple and for -Δ - b·∇ + c in TauCeti.Analysis.InnerProductSpace.Laplacian.LowerOrderMaximumPrinciple — perturb a subsolution by a barrier, take a maximizer of the perturbation over the compact set, and then argue that the frontier bound already holds at that maximizer. Only the last step is common: the two differ in how they produce the maximizer and in which barrier they use.

This module holds that step, stated once for the operator Δ + b·∇ with an arbitrary barrier. The -Δ + c principle runs it at b = 0 with the quadratic barrier ‖·‖².

It is a support module: TauCeti.le_of_isMaxOn_add_smul is support API for those two proofs rather than a result the roadmap asks for. Both principles import this module non-publicly, so neither re-exports it and nothing downstream of either principle sees the step in its interface.

theorem TauCeti.le_of_isMaxOn_add_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {K : Set E} {f w : E → ℝ} {v : E} {m ε : ℝ} {z : E} (hε : 0 < ε) (hcd : z ∈ interior K → ContDiffAt ℝ 2 f z) (hLf0 : z ∈ interior K → m < f z → 0 ≤ Laplacian.laplacian f z + (fderiv ℝ f z) v) (hbdry : z ∈ frontier K → f z ≤ m) (hzK : z ∈ K) (hwcd : z ∈ interior K → ContDiffAt ℝ 2 w z) (hwpos : z ∈ interior K → 0 < Laplacian.laplacian w z + (fderiv ℝ w z) v) (hzmax : IsMaxOn (fun (y : E) => f y + ε • w y) K z) : f z ≤ m

The maximizer step of the lower-order weak maximum principles. Let z be a maximizer of f + ε • w over K. If f z ≤ m whenever z is a frontier point, and, whenever z is interior and f z exceeds m, the operator Δ + ∇_v is nonnegative on f at z while the barrier w is C² and strictly positive under that operator at z, then f z ≤ m.

The direction is a single vector v, and the regularity and operator-sign hypotheses hcd, hLf0, hwcd, hwpos are asked for at z alone and only when z is interior. A caller holding the usual ∀ x ∈ interior K form instantiates it at z, as fun h => hcd h; a caller with a drift field b passes b z.