DivergenceLevelEnergy

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Superlevel energy for divergence forcing

This file derives the single-function superlevel gradient estimate for a zero-trace divergence-forced weak solution.

The existing predicate is used through its literal weak identity integral (a grad u) dot grad phi = integral g dot grad phi. In the standard distributional convention this is -div (a grad u) = -div g; the opposite forcing convention is obtained by replacing g with -g.

theorem HCPolySupport.IsZeroTraceDirichletRhsWeakSolution.levelEnergy_sumCoordNorm_le {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {a : CoeffField d} {lam Lam : ℝ} (hlam : 0 < lam) (hEll : IsEllipticFieldOn lam Lam U a) {u : H10Function U} {g : Vec d → Vec d} (hsol : IsZeroTraceDirichletRhsWeakSolution a U u g) (huMeas : Measurable u.toFun) (hg : MemVectorL2 U g) {M k : ℝ} (hM : 0 ≤ M) (hk : 0 ≤ k) (hgBound : ∀ᵐ (x : Vec d) ∂volumeMeasureOn U, √(vecNormSq (g x)) ≤ M) : ∑ i : Fin d, (MeasureTheory.eLpNorm ({x : Vec d | x ∈ U ∧ k < u.toFun x}.indicator fun (x : Vec d) => u.grad x i) 2 (volumeMeasureOn U)).toReal ≤ √↑d / lam * M * √(MeasureTheory.volume {x : Vec d | x ∈ U ∧ k < u.toFun x}).toReal

Under the displayed positive-sign weak identity, a bounded vector forcing controls the coordinate L² norms of the gradient on every nonnegative superlevel set.