CaccioppoliPlain

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

The Caccioppoli inequality at level zero

The De Giorgi cutoff estimates of CaccioppoliIdentity.lean, CaccioppoliInequality.lean and CaccioppoliAbsorbed.lean are stated for the positive part of a solution above a level. The statement below is the same estimate at the solution itself, with no truncation: testing -div (a grad u) = g against eta^2 u and absorbing half of the elliptic energy leaves lam / 2 * ∫ eta^2 |grad u|^2 ≤ ∫ g eta^2 u + (2 Lam^2 / lam) * ∫ u^2 |grad eta|^2.

The forcing term is kept signed, because the intended consumer has a nonpositive forcing (the difference of two Dirichlet resolvents of the same datum on two nested cubes solves the homogeneous shifted equation, whose forcing is a negative multiple of the solution). The right side is then quadratic in the solution, which turns the estimate into a Cauchy estimate.

theorem DivergenceFormProcess.Form.cutoff_energy_absorbed_plain {d : ℕ} {U : Set (HCPolySupport.Vec d)} {a : HCPolySupport.CoeffField d} {g : HCPolySupport.Vec d → ℝ} {u : HCPolySupport.H1Function U} (hsol : IsScalarForcedWeakSolution a U g u) (hU : HCPolySupport.IsOpenBoundedConvexDomain U) {lam Lam : ℝ} (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (eta : HCPolySupport.Vec d → ℝ) (heta : ContDiff ℝ (↑⊤) eta) (hetaCompact : HasCompactSupport eta) (hetaU : tsupport eta ⊆ U) : lam / 2 * ∫ (x : HCPolySupport.Vec d) in U, eta x ^ 2 * HCPolySupport.vecNormSq (u.grad x) ≤ (∫ (x : HCPolySupport.Vec d) in U, g x * (eta x ^ 2 * u.toFun x)) + 2 * Lam ^ 2 / lam * ∫ (x : HCPolySupport.Vec d) in U, u.toFun x ^ 2 * HCPolySupport.vecNormSq fun (i : Fin d) => (fderiv ℝ eta x) (HCPolySupport.basisVec i)

The Caccioppoli inequality at level zero. Half of the elliptic energy is absorbed and the forcing pairing is kept signed.