Coarse-graining support:

Support.Deterministic.CoarseCaccioppoli.EnergyBridge.DescendantSummationFullDual

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

Full-dual descendant summation

This sidecar is the corrected descendant summation corridor for the vector small-cube Caccioppoli route. It is parallel to the legacy projected theorem in DescendantSummation.lean, but the local estimate is supplied by the full-dual/local-multiscale exact-RHS theorem.

theorem HCPolySupport.abs_cubeAverage_vectorDot_scalarMultiply_le_raw_of_vectorFullDualLocalMultiscale {d : ℕ} {Q : TriadicCube d} (j : ℕ) (a : CoeffField d) (s : ℝ) {ρ₁ ρ₂ : ℝ} (flux : Vec d → Vec d) (u : Vec d → ℝ) (G : Vec d → Vec d) (energy : Vec d → ℝ) (η : QuantitativeCubeCutoff Q ρ₁ ρ₂) (Acirc1 AcircS : TriadicCube d → ℝ) {C K Alpha Bcross : ℝ} (hs0 : 0 < s) (hs1 : s < 1) (hpair_int : MeasureTheory.IntegrableOn (fun (x : Vec d) => vecDot (flux x) (u x • scalarCutoffGradientField η.toFun x)) (cubeSet Q) MeasureTheory.volume) (huQ : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x) (henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume) (hfluxMem : ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.MemLp flux 2 (normalizedCubeMeasure R)) (hu : ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.MemLp u 2 (normalizedCubeMeasure R)) (hG : ∀ R ∈ descendantsAtDepth Q j, ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => G x i) 2 (normalizedCubeMeasure R)) (hfluxEnergy : ∀ R ∈ descendantsAtDepth Q j, CoarseCaccioppoliFluxEnergyControls R a s flux energy) (hB : 0 ≤ quantitativeCubeCutoffHessianConst d / ((ρ₂ - ρ₁) * cubeRadius Q) ^ 2) (hAcirc1 : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ Acirc1 R) (hAcircS : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ AcircS R) (hBgConst : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ coarseCaccioppoliConstantCutoffSize R u (scalarCutoffGradientField η.toFun) (quantitativeCubeCutoffHessianConst d / ((ρ₂ - ρ₁) * cubeRadius Q) ^ 2)) (hBgCent : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ coarseCaccioppoliCenteredCutoffSize R s (scalarCutoffGradientField η.toFun) (Acirc1 R) (AcircS R) (√(cubeAverage R energy)) (quantitativeCubeCutoffHessianConst d / ((ρ₂ - ρ₁) * cubeRadius Q) ^ 2) (↑(Fintype.card (Fin d)) * C)) (hC : 0 ≤ C) (hfull : ∀ R ∈ descendantsAtDepth Q j, ∀ (N : ℕ), CubeDescendantDualFullVectorPoincareEstimate R C (cubeFluctuation R u) G N) (hlocal : ∀ R ∈ descendantsAtDepth Q j, ∀ (N : ℕ), CubeLocalMultiscalePoincareVectorEstimate R (3 / 2 * C * 3 ^ (↑d + 1)) (cubeFluctuation R u) G N) (hGcirc1 : ∀ R ∈ descendantsAtDepth Q j, ∀ (i : Fin d) (N : ℕ), (cubeBesovCircPartialNorm R 1 2 1 N fun (x : Vec d) => G x i) ≤ Acirc1 R * √(cubeAverage R energy)) (hGcircS : ∀ R ∈ descendantsAtDepth Q j, ∀ (i : Fin d) (N : ℕ), (cubeBesovCircPartialNorm R (1 - s) 2 1 N fun (x : Vec d) => G x i) ≤ AcircS R * √(cubeAverage R energy)) (hK_nonneg : 0 ≤ K) (hKparent : K * cubeLpNorm Q 2 u ≤ Bcross) (hconst : ∀ R ∈ descendantsAtDepth Q j, coarseCaccioppoliFluxEnergyExactConstantCoeff R a * (quantitativeCubeCutoffHessianConst d / ((ρ₂ - ρ₁) * cubeRadius Q) ^ 2 + cubeBesovScaleWeight 1 R * cubeLpNorm R ⊤ (scalarCutoffGradientField η.toFun)) ≤ K) (hcent : ∀ R ∈ descendantsAtDepth Q j, coarseCaccioppoliFluxEnergyExactCenteredCoeff R a s (scalarCutoffGradientField η.toFun) (Acirc1 R) (AcircS R) (quantitativeCubeCutoffHessianConst d / ((ρ₂ - ρ₁) * cubeRadius Q) ^ 2) (↑(Fintype.card (Fin d)) * C) ≤ Alpha) : |cubeAverage Q fun (x : Vec d) => vecDot (flux x) (u x • scalarCutoffGradientField η.toFun x)| ≤ Alpha * cubeAverage Q energy + Bcross * √(cubeAverage Q energy)

Variable-Acirc descendant raw estimate using full-dual vector Poincare and the finite local-multiscale estimate on every descendant.

theorem HCPolySupport.abs_cubeAverage_vectorDot_scalarMultiply_le_raw_of_support_buffer {d : ℕ} {Q : TriadicCube d} (j : ℕ) (a : CoeffField d) (s : ℝ) {ρ₁ ρ₂ ρ : ℝ} (flux : Vec d → Vec d) (u : Vec d → ℝ) (G : Vec d → Vec d) (energy : Vec d → ℝ) (η : QuantitativeCubeCutoff Q ρ₁ ρ₂) (Acirc1 AcircS : TriadicCube d → ℝ) {C K Alpha Bcross : ℝ} (hs0 : 0 < s) (hs1 : s < 1) (hbuffer : ∀ R ∈ descendantsAtDepth Q j, cubeScaleFactor R ≤ (ρ - ρ₂) * cubeRadius Q) (hpair_int : MeasureTheory.IntegrableOn (fun (x : Vec d) => vecDot (flux x) (u x • scalarCutoffGradientField η.toFun x)) (cubeSet Q) MeasureTheory.volume) (huQ : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x) (henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume) (hfluxMem : ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.MemLp flux 2 (normalizedCubeMeasure R)) (hu : ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.MemLp u 2 (normalizedCubeMeasure R)) (hG : ∀ R ∈ descendantsAtDepth Q j, ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => G x i) 2 (normalizedCubeMeasure R)) (hfluxEnergy : ∀ R ∈ descendantsAtDepth Q j, CoarseCaccioppoliFluxEnergyControls R a s flux energy) (hB : 0 ≤ quantitativeCubeCutoffHessianConst d / ((ρ₂ - ρ₁) * cubeRadius Q) ^ 2) (hAcirc1 : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ Acirc1 R) (hAcircS : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ AcircS R) (hBgConst : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ coarseCaccioppoliConstantCutoffSize R u (scalarCutoffGradientField η.toFun) (quantitativeCubeCutoffHessianConst d / ((ρ₂ - ρ₁) * cubeRadius Q) ^ 2)) (hBgCent : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ coarseCaccioppoliCenteredCutoffSize R s (scalarCutoffGradientField η.toFun) (Acirc1 R) (AcircS R) (√(cubeAverage R energy)) (quantitativeCubeCutoffHessianConst d / ((ρ₂ - ρ₁) * cubeRadius Q) ^ 2) (↑(Fintype.card (Fin d)) * C)) (hC : 0 ≤ C) (hfull : ∀ R ∈ descendantsAtDepth Q j, ∀ (N : ℕ), CubeDescendantDualFullVectorPoincareEstimate R C (cubeFluctuation R u) G N) (hGcirc1 : ∀ R ∈ descendantsAtDepth Q j, ∀ (i : Fin d) (N : ℕ), (cubeBesovCircPartialNorm R 1 2 1 N fun (x : Vec d) => G x i) ≤ Acirc1 R * √(cubeAverage R energy)) (hGcircS : ∀ R ∈ descendantsAtDepth Q j, ∀ (i : Fin d) (N : ℕ), (cubeBesovCircPartialNorm R (1 - s) 2 1 N fun (x : Vec d) => G x i) ≤ AcircS R * √(cubeAverage R energy)) (hK_nonneg : 0 ≤ K) (hKparent : K * cubeLpNorm Q 2 u ≤ Bcross) (hconst : ∀ R ∈ descendantsAtDepth Q j, coarseCaccioppoliFluxEnergyExactConstantCoeff R a * (quantitativeCubeCutoffHessianConst d / ((ρ₂ - ρ₁) * cubeRadius Q) ^ 2 + cubeBesovScaleWeight 1 R * cubeLpNorm R ⊤ (scalarCutoffGradientField η.toFun)) ≤ K) (hcent : ∀ R ∈ descendantsAtDepth Q j, coarseCaccioppoliFluxEnergyExactCenteredCoeff R a s (scalarCutoffGradientField η.toFun) (Acirc1 R) (AcircS R) (quantitativeCubeCutoffHessianConst d / ((ρ₂ - ρ₁) * cubeRadius Q) ^ 2) (↑(Fintype.card (Fin d)) * C) ≤ Alpha) : |cubeAverage Q fun (x : Vec d) => vecDot (flux x) (u x • scalarCutoffGradientField η.toFun x)| ≤ Alpha * coarseCaccioppoliLocalizedEnergyProfile Q ρ energy + Bcross * √(coarseCaccioppoliLocalizedEnergyProfile Q ρ energy)

Buffered localized-energy descendant summation using full-dual Poincare and the infinite-depth full-circ route on every descendant.

theorem HCPolySupport.abs_cubeAverage_vectorDot_scalarMultiply_le_local_raw {d : ℕ} {Q : TriadicCube d} (center : Vec d) (j : ℕ) (a : CoeffField d) (s : ℝ) {rhoInner rhoOuter rho : ℝ} (flux : Vec d → Vec d) (u : Vec d → ℝ) (G : Vec d → Vec d) (energy : Vec d → ℝ) (Acirc1 AcircS : TriadicCube d → ℝ) {C K Alpha Bcross : ℝ} (hinner : 0 < rhoInner) (hinnerOuter : rhoInner < rhoOuter) (hs0 : 0 < s) (hs1 : s < 1) (hbuffer : ∀ R ∈ descendantsAtDepth Q j, cubeScaleFactor R ≤ (rho - rhoOuter) * (cubeRadius Q / 3)) (hpair_int : MeasureTheory.IntegrableOn (fun (x : Vec d) => vecDot (flux x) (u x • scalarCutoffGradientField (coarseCaccioppoliLocalCanonicalFun Q center rhoInner rhoOuter) x)) (cubeSet Q) MeasureTheory.volume) (huQ : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x) (henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume) (hfluxMem : ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.MemLp flux 2 (normalizedCubeMeasure R)) (hu : ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.MemLp u 2 (normalizedCubeMeasure R)) (hG : ∀ R ∈ descendantsAtDepth Q j, ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => G x i) 2 (normalizedCubeMeasure R)) (hfluxEnergy : ∀ R ∈ descendantsAtDepth Q j, CoarseCaccioppoliFluxEnergyControls R a s flux energy) (hB : 0 ≤ quantitativeCubeCutoffHessianConst d / ((rhoOuter - rhoInner) * (cubeRadius Q / 3)) ^ 2) (hAcirc1 : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ Acirc1 R) (hAcircS : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ AcircS R) (hBgConst : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ coarseCaccioppoliConstantCutoffSize R u (scalarCutoffGradientField (coarseCaccioppoliLocalCanonicalFun Q center rhoInner rhoOuter)) (quantitativeCubeCutoffHessianConst d / ((rhoOuter - rhoInner) * (cubeRadius Q / 3)) ^ 2)) (hBgCent : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ coarseCaccioppoliCenteredCutoffSize R s (scalarCutoffGradientField (coarseCaccioppoliLocalCanonicalFun Q center rhoInner rhoOuter)) (Acirc1 R) (AcircS R) (√(cubeAverage R energy)) (quantitativeCubeCutoffHessianConst d / ((rhoOuter - rhoInner) * (cubeRadius Q / 3)) ^ 2) (↑(Fintype.card (Fin d)) * C)) (hC : 0 ≤ C) (hfull : ∀ R ∈ descendantsAtDepth Q j, ∀ (N : ℕ), CubeDescendantDualFullVectorPoincareEstimate R C (cubeFluctuation R u) G N) (hGcirc1 : ∀ R ∈ descendantsAtDepth Q j, ∀ (i : Fin d) (N : ℕ), (cubeBesovCircPartialNorm R 1 2 1 N fun (x : Vec d) => G x i) ≤ Acirc1 R * √(cubeAverage R energy)) (hGcircS : ∀ R ∈ descendantsAtDepth Q j, ∀ (i : Fin d) (N : ℕ), (cubeBesovCircPartialNorm R (1 - s) 2 1 N fun (x : Vec d) => G x i) ≤ AcircS R * √(cubeAverage R energy)) (hK_nonneg : 0 ≤ K) (hKparent : K * cubeLpNorm Q 2 u ≤ Bcross) (hconst : ∀ R ∈ descendantsAtDepth Q j, coarseCaccioppoliFluxEnergyExactConstantCoeff R a * (quantitativeCubeCutoffHessianConst d / ((rhoOuter - rhoInner) * (cubeRadius Q / 3)) ^ 2 + cubeBesovScaleWeight 1 R * cubeLpNorm R ⊤ (scalarCutoffGradientField (coarseCaccioppoliLocalCanonicalFun Q center rhoInner rhoOuter))) ≤ K) (hcent : ∀ R ∈ descendantsAtDepth Q j, coarseCaccioppoliFluxEnergyExactCenteredCoeff R a s (scalarCutoffGradientField (coarseCaccioppoliLocalCanonicalFun Q center rhoInner rhoOuter)) (Acirc1 R) (AcircS R) (quantitativeCubeCutoffHessianConst d / ((rhoOuter - rhoInner) * (cubeRadius Q / 3)) ^ 2) (↑(Fintype.card (Fin d)) * C) ≤ Alpha) : |cubeAverage Q fun (x : Vec d) => vecDot (flux x) (u x • scalarCutoffGradientField (coarseCaccioppoliLocalCanonicalFun Q center rhoInner rhoOuter) x)| ≤ Alpha * coarseCaccioppoliLocalEnergyProfile Q center rho energy + Bcross * √(coarseCaccioppoliLocalEnergyProfile Q center rho energy)

Buffered arbitrary-center local-patch descendant summation for the translated canonical cutoff using the full-dual/full-circ route.