Coarse-graining support:

Support.Deterministic.CoarseCaccioppoli.SingleCubeToRaw.HarmonicFinal.InputSpecializations .LocalPatchNoteRawBridge

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

Local-patch note raw bridge

This sidecar ties the arbitrary-center local-patch descendant summation to the harmonic weak-testing identity. It covers the interior-contained local patch case: the translated cutoff support is required to lie inside the parent open cube, so the compact-support test function is admissible without a boundary zero-trace argument.

theorem HCPolySupport.CoarseCaccioppoliBoundaryCanonicalHarmonicVectorLocalPatchNoteRawBridgeSplit.of_constantFamily_bufferedSmallCubeCoefficientBoundsSplit_of_zeroTrace {d : ℕ} [NeZero d] (Q : TriadicCube d) (center : Vec d) (a : CoeffField d) (s t Clocal Calpha Ccross : ℝ) {lam Lam : ℝ} {V : Set (Vec d)} (u0 : AHarmonicFunction a (openCubeSet Q)) (hzero : LocalizedZeroTraceFunctionOn (openCubeSet Q) V u0.toH1.toFun) (hClocal : 0 ≤ Clocal) (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) (hcutoffWindow : ∀ (n : ℕ), have ρ₁ := coarseCaccioppoliRadiusSequence n; have ρ₂ := coarseCaccioppoliRadiusSequence (n + 1); have ρm := coarseCaccioppoliBufferedCutoffRadius ρ₁ ρ₂; coarseCaccioppoliLocalClosedCube Q center ρm ⊆ V) (hrawcoeff : boundaryCaccioppoliSmallCubeLocalPatchCoefficientSplit Q center a s t Clocal Calpha Ccross) : CoarseCaccioppoliBoundaryCanonicalHarmonicVectorLocalPatchNoteRawBridgeSplit Q center a s t Calpha Ccross (coarseCaccioppoliHarmonicL2Sq Q a u0) fun (x : Vec d) => scalarVariationEnergyIntegrand a u0 x

Boundary local-patch split raw bridge for a constant harmonic family, in the boundary-touching case supplied by a localized scalar zero-trace condition.

theorem HCPolySupport.CoarseCaccioppoliBoundaryCanonicalHarmonicVectorLocalPatchNoteRawBridgeSplitAllRadii.of_constantFamily_bufferedSmallCubeCoefficientBoundsSplitAllRadii_of_zeroTrace {d : ℕ} [NeZero d] (Q : TriadicCube d) (center : Vec d) (a : CoeffField d) (s t Clocal Calpha Ccross : ℝ) {lam Lam : ℝ} {V : Set (Vec d)} (u0 : AHarmonicFunction a (openCubeSet Q)) (hzero : LocalizedZeroTraceFunctionOn (openCubeSet Q) V u0.toH1.toFun) (hClocal : 0 ≤ Clocal) (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) (hcutoffWindow : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → have ρm := coarseCaccioppoliBufferedCutoffRadius ρ₁ ρ₂; coarseCaccioppoliLocalClosedCube Q center ρm ⊆ V) (hrawcoeff : boundaryCaccioppoliSmallCubeLocalPatchCoefficientSplitAllRadii Q center a s t Clocal Calpha Ccross) : CoarseCaccioppoliBoundaryCanonicalHarmonicVectorLocalPatchNoteRawBridgeSplitAllRadii Q center a s t Calpha Ccross (coarseCaccioppoliHarmonicL2Sq Q a u0) fun (x : Vec d) => scalarVariationEnergyIntegrand a u0 x

All-radii boundary local-patch split raw bridge for a constant harmonic family, in the boundary-touching case supplied by a localized scalar zero-trace condition.

theorem HCPolySupport.coarseCaccioppoli_boundary_local_qone_standard_le_noteRhs_explicitSplit {d : ℕ} [NeZero d] (Q : TriadicCube d) (center : Vec d) (a : CoeffField d) (s t Clocal Calpha Ccross : ℝ) {lam Lam : ℝ} (u0 : AHarmonicFunction a (openCubeSet Q)) (hzero : LocalizedZeroTraceFunctionOn (openCubeSet Q) (coarseCaccioppoliLocalOpenCube Q center 1) u0.toH1.toFun) (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 : boundaryCaccioppoliSmallCubeLocalPatchCoefficientSplitAllRadii Q center a s t Clocal Calpha Ccross) : coarseCaccioppoliLocalEnergyRadiusProfile Q center (fun (x : Vec d) => scalarVariationEnergyIntegrand a u0 x) (1 / 3) ≤ coarseCaccioppoliBoundaryNoteRhs Q a s t (coarseCaccioppoliBoundaryStandardExplicitNoteConstantSplit Q a s t (↑(Fintype.card (Fin d)) * Calpha) (↑(Fintype.card (Fin d)) * Ccross)) (coarseCaccioppoliHarmonicL2Sq Q a u0)

Boundary local-patch standard note-RHS endpoint for a constant harmonic family with zero trace on the full local cu_{m-1} window, with split note coefficients.