Coarse-graining support:

Support.Deterministic.CoarseCaccioppoli.SingleCubeToRaw.HarmonicFinal.ExactSmallCube .LocalPatchConstructor

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Local-patch exact small-cube coefficient constructors

This file contains the final coefficient-package constructors for the arbitrary-center local-patch exact small-cube route. Factor and branch estimates live in the LocalPatchConstructor/ submodules.

theorem HCPolySupport.boundaryCaccioppoliSmallCubeLocalPatchCoefficientSplit.of_closedCubeEllipticity_of_localPatchBufferedCutoffRadiusConst_of_centeredFronts {d : ℕ} [NeZero d] (Q : TriadicCube d) (center : Vec d) (a : CoeffField d) (s t Clocal Calpha Ccross : ℝ) {lam Lam : ℝ} (hClocal : 0 ≤ Clocal) (hCalpha : 0 ≤ Calpha) (hwork_constant_cross : 81 * Real.rpow 3 (2 * s) * (↑(Fintype.card (Fin d)) * Clocal) ≤ ↑(Fintype.card (Fin d)) * Ccross) (hwork_centered_fronts_alpha : 81 * (6 * coarseCaccioppoliCenteredAverageFront d s (↑(Fintype.card (Fin d)) * Clocal) + 12 * coarseCaccioppoliCenteredBesovHessianFront d s (↑(Fintype.card (Fin d)) * Clocal) + 6 * coarseCaccioppoliCenteredBesovGradientFront d s (↑(Fintype.card (Fin d)) * Clocal)) ≤ ↑(Fintype.card (Fin d)) * Calpha / (s * (1 - s))) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hEllCube : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hlarge : ↑d * 3 ^ (↑d + 1) * (geometricDiscount 1 1)⁻¹ * (12 * (quantitativeCubeCutoffHessianConst d * cubeScaleFactor Q / cubeRadius Q ^ 2) + 6 * (quantitativeCubeCutoffGradientConst d / cubeRadius Q)) ≤ ↑(Fintype.card (Fin d)) * Clocal) : boundaryCaccioppoliSmallCubeLocalPatchCoefficientSplit Q center a s t Clocal Calpha Ccross

Direct split local-patch exact-to-parent-raw coefficient bounds from closed-cube ellipticity.

The constant branch is paid by Ccross, while the centered branch and the integerized height are paid by Calpha.

theorem HCPolySupport.boundaryCaccioppoliSmallCubeLocalPatchCoefficientSplitAllRadii.of_closedCubeEllipticity_of_localPatchBufferedCutoffRadiusConst_of_centeredFronts {d : ℕ} [NeZero d] (Q : TriadicCube d) (center : Vec d) (a : CoeffField d) (s t Clocal Calpha Ccross : ℝ) {lam Lam : ℝ} (hClocal : 0 ≤ Clocal) (hCalpha : 0 ≤ Calpha) (hwork_constant_cross : 81 * Real.rpow 3 (2 * s) * (↑(Fintype.card (Fin d)) * Clocal) ≤ ↑(Fintype.card (Fin d)) * Ccross) (hwork_centered_fronts_alpha : 81 * (6 * coarseCaccioppoliCenteredAverageFront d s (↑(Fintype.card (Fin d)) * Clocal) + 12 * coarseCaccioppoliCenteredBesovHessianFront d s (↑(Fintype.card (Fin d)) * Clocal) + 6 * coarseCaccioppoliCenteredBesovGradientFront d s (↑(Fintype.card (Fin d)) * Clocal)) ≤ ↑(Fintype.card (Fin d)) * Calpha / (s * (1 - s))) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hEllCube : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hlarge : ↑d * 3 ^ (↑d + 1) * (geometricDiscount 1 1)⁻¹ * (12 * (quantitativeCubeCutoffHessianConst d * cubeScaleFactor Q / cubeRadius Q ^ 2) + 6 * (quantitativeCubeCutoffGradientConst d / cubeRadius Q)) ≤ ↑(Fintype.card (Fin d)) * Clocal) : boundaryCaccioppoliSmallCubeLocalPatchCoefficientSplitAllRadii Q center a s t Clocal Calpha Ccross

All-radii direct split local-patch exact-to-parent-raw coefficient bounds from closed-cube ellipticity.

This is the proof-producing coefficient package for the standard radius iteration in the arbitrary-center boundary route.