Theory #
Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.
Public Coarse Caccioppoli with RHS Theory #
This file is split mechanically out of CoarseCaccioppoliRHS.lean.
Audit tag #
Claim: expose the single public boundary coarse Caccioppoli-with-RHS theorem
package and assemble it from the proved parent-L² corrector bound.
Downstream target: note-facing Ch3 theorem consumers. This is the only public
CoarseCaccioppoliRHSTheory surface; new variants must amend the Ch3 surface
contract first.
Public theorem package for the boundary coarse-grained Caccioppoli estimate with right-hand side.
- exists_constant : ∃ (C : ℝ), 0 < C ∧ ∀ {Q : TriadicCube d} {a : CoeffFamily d} {s t : ℝ} {x : Vec d} {g : Vec d → Vec d} (u : BoundaryForcedCaccioppoliDatum Q a x g), 0 < s → s < 1 → 0 < t → t < 1 / 2 → s + t < 1 → x ∈ openCubeSet Q → ForceBesovRegularity Q (2 * t) g → boundaryForcedCaccioppoliCoreEnergy u ≤ boundaryCaccioppoliWithRHSRHS C s t u
Instances For
Proved public coarse-grained boundary Caccioppoli estimate with right-hand side.