Coarse-graining support: Support.Book.Ch03.Theorems.CoarseCaccioppoliScaleZeroBridge #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Scale-zero Caccioppoli public bridge estimates #
This file assembles the scale-zero core estimates with the RHS bridge helpers and explicit scalar envelope to produce the public scale-zero Caccioppoli endpoint used by the dilation transport layer.
Audit tag #
Claim: bridge deterministic scale-zero core estimates and explicit scalar budgets into the public boundary and centered-interior RHS forms.
Downstream target: coarseCaccioppoliScaleZeroTheory_of_scalarEnvelope.
This file is bridge plumbing only; it should not introduce another public
*Theory package.
theorem
HCPolySupport.Book.Ch03.boundary_publicCoreEnergy_le_publicRHS_of_scale_zero_of_unitStandardExplicitBoundSplit
{d : ℕ}
[NeZero d]
{Q : TriadicCube d}
{a : CoeffFamily d}
{x : Vec d}
(u : BoundaryCaccioppoliDatum Q a x)
{s t C : ℝ}
(hs : 0 < s)
(ht : 0 < t)
(hst : s + t < 1)
(hx : x ∈ openCubeSet Q)
(hQscale : Q.scale = 0)
(hC :
have CalphaInternal := ↑(Fintype.card (Fin d)) * coarseCaccioppoliLocalPatchBufferedAlphaBudgetUnit d s;
have CcrossInternal := ↑(Fintype.card (Fin d)) * coarseCaccioppoliLocalPatchBufferedCrossBudgetUnit d s;
18 ^ d * (↑d ^ 2 * caccioppoliStandardExplicitNoteBoundSplit s t CalphaInternal CcrossInternal) ≤ C)
:
theorem
HCPolySupport.Book.Ch03.interiorCoreEnergy_le_RHS_of_standardBudget
{d : ℕ}
[NeZero d]
{Q : TriadicCube d}
{a : CoeffFamily d}
(u : CubeSolution Q a)
{s t C : ℝ}
(hs : 0 < s)
(ht : 0 < t)
(hst : s + t < 1)
(hQscale : Q.scale = 0)
(hC :
have CalphaInternal := ↑(Fintype.card (Fin d)) * coarseCaccioppoliBufferedAlphaBudgetUnit d s;
have CcrossInternal := ↑(Fintype.card (Fin d)) * coarseCaccioppoliBufferedCrossBudgetUnit d s;
18 ^ d * (↑d ^ 2 * caccioppoliStandardExplicitNoteBoundSplit s t CalphaInternal CcrossInternal) ≤ C)
: