Coarse-graining support:

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

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_testing {d : ℕ} [NeZero d] (Q : TriadicCube d) (center : Vec d) (a : CoeffField d) (s t Clocal Calpha Ccross : ℝ) {lam Lam : ℝ} (u0 : AHarmonicFunction a (openCubeSet Q)) (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) (htesting : ∀ (n : ℕ), have ρ₁ := coarseCaccioppoliRadiusSequence n; have ρ₂ := coarseCaccioppoliRadiusSequence (n + 1); have ρm := coarseCaccioppoliBufferedCutoffRadius ρ₁ ρ₂; have energy := fun (x : Vec d) => scalarVariationEnergyIntegrand a u0 x; have flux := fun (x : Vec d) => matVecMul (a x) (u0.toH1.grad x); have u := fun (x : Vec d) => u0.toH1.toFun x; have ξ := scalarCutoffGradientField (coarseCaccioppoliLocalCanonicalFun Q center ρ₁ ρm); coarseCaccioppoliLocalEnergyRadiusProfile Q center energy ρ₁ ≤ |cubeAverage Q fun (x : Vec d) => vecDot (flux x) (u x • ξ x)|) (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 raw bridge for a constant harmonic family with split note coefficients, once the local weak-testing estimate has been supplied at every radius.

theorem HCPolySupport.CoarseCaccioppoliBoundaryCanonicalHarmonicVectorLocalPatchNoteRawBridgeSplitAllRadii.of_constantFamily_bufferedSmallCubeCoefficientBoundsSplitAllRadii_of_testing {d : ℕ} [NeZero d] (Q : TriadicCube d) (center : Vec d) (a : CoeffField d) (s t Clocal Calpha Ccross : ℝ) {lam Lam : ℝ} (u0 : AHarmonicFunction a (openCubeSet Q)) (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) (htesting : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → have ρm := coarseCaccioppoliBufferedCutoffRadius ρ₁ ρ₂; have energy := fun (x : Vec d) => scalarVariationEnergyIntegrand a u0 x; have flux := fun (x : Vec d) => matVecMul (a x) (u0.toH1.grad x); have u := fun (x : Vec d) => u0.toH1.toFun x; have ξ := scalarCutoffGradientField (coarseCaccioppoliLocalCanonicalFun Q center ρ₁ ρm); coarseCaccioppoliLocalEnergyRadiusProfile Q center energy ρ₁ ≤ |cubeAverage Q fun (x : Vec d) => vecDot (flux x) (u x • ξ x)|) (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 raw bridge for a constant harmonic family with split note coefficients, once the local weak-testing estimate has been supplied at every admissible radius pair.