Coarse-graining support:

Support.Deterministic.CoarseCaccioppoli.SingleCubeToRaw.HarmonicFinal.InputSpecializations .NoteRawBridge

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

theorem HCPolySupport.CoarseCaccioppoliInteriorCanonicalHarmonicVectorNoteRawBridgeSplit.of_smallCubeBoundsSplit {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s t Clocal Calpha Ccross : ℝ) {lam Lam : ℝ} (u0 : AHarmonicFunction a (openCubeSet Q)) (hClocal : 0 ≤ Clocal) (hCalpha : 0 ≤ Calpha) (hCcross : 0 ≤ Ccross) (hCsol_le : fullVectorPoincareCubeConstant Q ≤ Clocal) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hEllCube : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hrawcoeff : BoundaryCaccioppoliHarmonicVectorSmallCubeCoefficientSplit Q a s t Clocal Calpha Ccross) : CoarseCaccioppoliInteriorCanonicalHarmonicVectorNoteRawBridgeSplit Q a s t Calpha Ccross (coarseCaccioppoliHarmonicL2Sq Q a u0) fun (x : Vec d) => scalarVariationEnergyIntegrand a u0 x

Split interior raw bridge for a constant harmonic family using the same buffered localized-energy summation as the repaired boundary route.

theorem HCPolySupport.coarseCaccioppoli_boundary_qone_standard_le_noteRhs_explicitSplit {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s t Calpha Ccross uL2Sq : ℝ) {lam Lam : ℝ} (baseEnergy : Vec d → ℝ) (w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q)) (hCalpha : 0 < Calpha) (hCcross : 0 ≤ Ccross) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) (hEllCube : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hProfile : CoarseCaccioppoliBoundaryCanonicalHarmonicProfileInputs Q a baseEnergy w) (hBridge : CoarseCaccioppoliBoundaryCanonicalHarmonicVectorNoteRawBridgeSplitAllRadii Q a s t Calpha Ccross uL2Sq baseEnergy) : coarseCaccioppoliLocalizedEnergyRadiusProfile Q baseEnergy (1 / 3) ≤ coarseCaccioppoliBoundaryNoteRhs Q a s t (coarseCaccioppoliBoundaryStandardExplicitNoteConstantSplit Q a s t (↑(Fintype.card (Fin d)) * Calpha) (↑(Fintype.card (Fin d)) * Ccross)) uL2Sq

Boundary note-RHS Caccioppoli from an all-radii split note-faithful raw bridge, using the standard beta-dependent radius iteration.

theorem HCPolySupport.coarseCaccioppoli_interior_qone_standard_le_noteRhs_explicitSplit {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s t Calpha Ccross uL2Sq : ℝ) {lam Lam : ℝ} (baseEnergy : Vec d → ℝ) (w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q)) (hCalpha : 0 < Calpha) (hCcross : 0 ≤ Ccross) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) (hEllCube : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hProfile : CoarseCaccioppoliBoundaryCanonicalHarmonicProfileInputs Q a baseEnergy w) (hBridge : CoarseCaccioppoliInteriorCanonicalHarmonicVectorNoteRawBridgeSplitAllRadii Q a s t Calpha Ccross uL2Sq baseEnergy) : coarseCaccioppoliLocalizedEnergyRadiusProfile Q baseEnergy (1 / 3) ≤ coarseCaccioppoliInteriorNoteRhs Q a s t (coarseCaccioppoliBoundaryStandardExplicitNoteConstantSplit Q a s t (↑(Fintype.card (Fin d)) * Calpha) (↑(Fintype.card (Fin d)) * Ccross)) uL2Sq

Interior note-RHS Caccioppoli from an all-radii split note-faithful raw bridge, using the standard beta-dependent radius iteration.

theorem HCPolySupport.coarseCaccioppoli_boundary_local_qone_standard_le_of_noteBridgeSplitAllRadii {d : ℕ} [NeZero d] (Q : TriadicCube d) (center : Vec d) (a : CoeffField d) (s t Calpha Ccross uL2Sq : ℝ) {lam Lam : ℝ} (baseEnergy : Vec d → ℝ) (w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q)) (hCalpha : 0 < Calpha) (hCcross : 0 ≤ Ccross) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) (hEllCube : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hbase_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ baseEnergy x) (hbase_int : MeasureTheory.IntegrableOn baseEnergy (cubeSet Q) MeasureTheory.volume) (hBridge : CoarseCaccioppoliBoundaryCanonicalHarmonicVectorLocalPatchNoteRawBridgeSplitAllRadii Q center a s t Calpha Ccross uL2Sq baseEnergy) : coarseCaccioppoliLocalEnergyRadiusProfile Q center baseEnergy (1 / 3) ≤ coarseCaccioppoliBoundaryNoteRhs Q a s t (coarseCaccioppoliBoundaryStandardExplicitNoteConstantSplit Q a s t (↑(Fintype.card (Fin d)) * Calpha) (↑(Fintype.card (Fin d)) * Ccross)) uL2Sq

Boundary note-RHS Caccioppoli from an all-radii split arbitrary-center local-patch raw bridge, using the standard beta-dependent radius iteration.

The theorem-facing endpoint aliases that used to live here are now in HarmonicFinal/Endpoints.lean. This file now stops at the internal bridge constructors and compatibility plumbing that those endpoints consume.