Coarse-graining support:

Support.Deterministic.CoarseCaccioppoli.SingleCubeToRaw.LocalPatchWeakTesting

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

Weak testing with arbitrary-center local Caccioppoli cutoffs

This file specializes the parent-cube weak testing identity to the translated local canonical cutoffs used in the boundary Caccioppoli proof. The only geometric input is that the local outer closed cube is still contained in the parent open cube, so the product cutoff is an admissible compactly supported test function in the parent cube.

theorem HCPolySupport.integrableOn_vecDot_harmonicFlux_harmonicFunction_localCanonicalCutoff {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) {lam Lam : ℝ} (center : Vec d) {rhoInner rhoOuter : ℝ} (w : AHarmonicFunction a (openCubeSet Q)) (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hinner : 0 < rhoInner) (hinnerOuter : rhoInner < rhoOuter) : MeasureTheory.IntegrableOn (fun (x : Vec d) => vecDot (matVecMul (a x) (w.toH1.grad x)) (w.toH1.toFun x • scalarCutoffGradientField (coarseCaccioppoliLocalCanonicalFun Q center rhoInner rhoOuter) x)) (cubeSet Q) MeasureTheory.volume

The harmonic flux paired with the arbitrary-center local cutoff gradient is integrable on the parent cube.

theorem HCPolySupport.le_abs_cubeAverage_vectorDot_flux_localCanonicalCutoff_of_aHarmonicFunction {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) {lam Lam F : ℝ} (center : Vec d) {rhoInner rhoOuter : ℝ} (w : AHarmonicFunction a (openCubeSet Q)) (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hinner : 0 < rhoInner) (hinnerOuter : rhoInner < rhoOuter) (hsub : coarseCaccioppoliLocalClosedCube Q center rhoOuter ⊆ openCubeSet Q) (hlower : F ≤ cubeAverage Q fun (x : Vec d) => coarseCaccioppoliLocalCanonicalFun Q center rhoInner rhoOuter x * scalarVariationEnergyIntegrand a w x) : F ≤ |cubeAverage Q fun (x : Vec d) => vecDot (matVecMul (a x) (w.toH1.grad x)) (w.toH1.toFun x • scalarCutoffGradientField (coarseCaccioppoliLocalCanonicalFun Q center rhoInner rhoOuter) x)|

Local-cutoff weak testing for an arbitrary patch center whose outer local closed cube stays inside the parent open cube.

theorem HCPolySupport.le_abs_cubeAverage_vectorDot_flux_localCanonicalCutoff_of_of_aHarmonicFunction {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) {lam Lam F : ℝ} (center : Vec d) {rhoInner rhoOuter : ℝ} (w : AHarmonicFunction a (openCubeSet Q)) (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) {V : Set (Vec d)} (hzero : LocalizedZeroTraceFunctionOn (openCubeSet Q) V w.toH1.toFun) (hinner : 0 < rhoInner) (hinnerOuter : rhoInner < rhoOuter) (hsub : coarseCaccioppoliLocalClosedCube Q center rhoOuter ⊆ V) (hlower : F ≤ cubeAverage Q fun (x : Vec d) => coarseCaccioppoliLocalCanonicalFun Q center rhoInner rhoOuter x * scalarVariationEnergyIntegrand a w x) : F ≤ |cubeAverage Q fun (x : Vec d) => vecDot (matVecMul (a x) (w.toH1.grad x)) (w.toH1.toFun x • scalarCutoffGradientField (coarseCaccioppoliLocalCanonicalFun Q center rhoInner rhoOuter) x)|

Local-cutoff weak testing for a boundary-touching patch. Instead of requiring the outer local closed cube to sit inside the parent open cube, this uses a localized scalar zero-trace hypothesis to make the cutoff product an admissible H¹₀ test function.