Coarse-graining support:

Support.Deterministic.CoarseCaccioppoli.EnergyBridge.DescendantSummation.ExactRhs

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

Descendant summation for the small-cube Caccioppoli route

The LaTeX proof estimates the cutoff pairing on small cubes and then sums over those cubes. This file isolates the measure-theoretic bookkeeping: a cube-average over Q is the descendants-average of the cube-averages over the depth-j descendants, hence its absolute value is controlled by the descendants-average of the local absolute values.

theorem HCPolySupport.descendantsAverage_fluxEnergyExactRhs_le_raw_of_pointwise_coefficients {d : ℕ} (Q : TriadicCube d) (j : ℕ) (a : CoeffField d) (s : ℝ) (u : Vec d → ℝ) (ξ : Vec d → Vec d) (energy : Vec d → ℝ) (Acirc1 AcircS B C K Alpha Bcross : ℝ) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x) (henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume) (hK_nonneg : 0 ≤ K) (hKparent : K * cubeLpNorm Q 2 u ≤ Bcross) (hconst : ∀ R ∈ descendantsAtDepth Q j, coarseCaccioppoliFluxEnergyExactConstantCoeff R a * (B + cubeBesovScaleWeight 1 R * cubeLpNorm R ⊤ ξ) ≤ K) (hcent : ∀ R ∈ descendantsAtDepth Q j, coarseCaccioppoliFluxEnergyExactCenteredCoeff R a s ξ Acirc1 AcircS B C ≤ Alpha) : (descendantsAverage Q j fun (R : TriadicCube d) => coarseCaccioppoliFluxEnergyExactRhs R a s u ξ energy Acirc1 AcircS B C) ≤ Alpha * cubeAverage Q energy + Bcross * √(cubeAverage Q energy)

Collapse a descendant average of exact flux-energy RHS values to the parent raw-recursion RHS.

This is the core small-cube summation step. The constant branch is summed by finite Cauchy, so it only needs the parent L² norm of u; the centered branch collapses by additivity of the energy average.

theorem HCPolySupport.descendantsAverage_fluxEnergyExactRhs_le_raw_of_pointwise_coefficients_variableAcirc {d : ℕ} (Q : TriadicCube d) (j : ℕ) (a : CoeffField d) (s : ℝ) (u : Vec d → ℝ) (ξ : Vec d → Vec d) (energy : Vec d → ℝ) (Acirc1 AcircS : TriadicCube d → ℝ) (B C K Alpha Bcross : ℝ) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x) (henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume) (hK_nonneg : 0 ≤ K) (hKparent : K * cubeLpNorm Q 2 u ≤ Bcross) (hconst : ∀ R ∈ descendantsAtDepth Q j, coarseCaccioppoliFluxEnergyExactConstantCoeff R a * (B + cubeBesovScaleWeight 1 R * cubeLpNorm R ⊤ ξ) ≤ K) (hcent : ∀ R ∈ descendantsAtDepth Q j, coarseCaccioppoliFluxEnergyExactCenteredCoeff R a s ξ (Acirc1 R) (AcircS R) B C ≤ Alpha) : (descendantsAverage Q j fun (R : TriadicCube d) => coarseCaccioppoliFluxEnergyExactRhs R a s u ξ energy (Acirc1 R) (AcircS R) B C) ≤ Alpha * cubeAverage Q energy + Bcross * √(cubeAverage Q energy)

Variable-Acirc version of descendantsAverage_fluxEnergyExactRhs_le_raw_of_pointwise_coefficients.

The exact RHS on each descendant uses the local values Acirc1 R and AcircS R; the endpoint raw RHS is unchanged.

theorem HCPolySupport.descendantsAverage_fluxEnergyExactRhs_le_localized_raw_of_pointwise_coefficients_variableAcirc {d : ℕ} (Q : TriadicCube d) (j : ℕ) (ρ : ℝ) (a : CoeffField d) (s : ℝ) (u : Vec d → ℝ) (ξ : Vec d → Vec d) (energy : Vec d → ℝ) (Acirc1 AcircS : TriadicCube d → ℝ) (B C K Alpha Bcross : ℝ) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x) (henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume) (hK_nonneg : 0 ≤ K) (hKparent : K * cubeLpNorm Q 2 u ≤ Bcross) (hconst : ∀ R ∈ descendantsAtDepth Q j, coarseCaccioppoliFluxEnergyExactConstantCoeff R a * (B + cubeBesovScaleWeight 1 R * cubeLpNorm R ⊤ ξ) ≤ K) (hcent : ∀ R ∈ descendantsAtDepth Q j, coarseCaccioppoliFluxEnergyExactCenteredCoeff R a s ξ (Acirc1 R) (AcircS R) B C ≤ Alpha) : (descendantsAverage Q j fun (R : TriadicCube d) => coarseCaccioppoliFluxEnergyExactRhs R a s u ξ ((scaledClosedCubeSet Q ρ).indicator energy) (Acirc1 R) (AcircS R) B C) ≤ Alpha * coarseCaccioppoliLocalizedEnergyProfile Q ρ energy + Bcross * √(coarseCaccioppoliLocalizedEnergyProfile Q ρ energy)

Localized-energy version of the variable-Acirc exact-RHS descendant collapse. The local RHS values use the energy density cut down to the outer scaled cube, so the endpoint is the outer localized profile rather than the full parent cube average.

theorem HCPolySupport.descendantsAverage_fluxEnergyExactRhs_le_localPatch_raw_of_pointwise_coefficients_variableAcirc {d : ℕ} (Q : TriadicCube d) (center : Vec d) (j : ℕ) (rho : ℝ) (a : CoeffField d) (s : ℝ) (u : Vec d → ℝ) (ξ : Vec d → Vec d) (energy : Vec d → ℝ) (Acirc1 AcircS : TriadicCube d → ℝ) (B C K Alpha Bcross : ℝ) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x) (henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume) (hK_nonneg : 0 ≤ K) (hKparent : K * cubeLpNorm Q 2 u ≤ Bcross) (hconst : ∀ R ∈ descendantsAtDepth Q j, coarseCaccioppoliFluxEnergyExactConstantCoeff R a * (B + cubeBesovScaleWeight 1 R * cubeLpNorm R ⊤ ξ) ≤ K) (hcent : ∀ R ∈ descendantsAtDepth Q j, coarseCaccioppoliFluxEnergyExactCenteredCoeff R a s ξ (Acirc1 R) (AcircS R) B C ≤ Alpha) : (descendantsAverage Q j fun (R : TriadicCube d) => coarseCaccioppoliFluxEnergyExactRhs R a s u ξ ((coarseCaccioppoliLocalClosedCube Q center rho).indicator energy) (Acirc1 R) (AcircS R) B C) ≤ Alpha * coarseCaccioppoliLocalEnergyProfile Q center rho energy + Bcross * √(coarseCaccioppoliLocalEnergyProfile Q center rho energy)

Arbitrary-center local-patch version of the variable-Acirc exact-RHS descendant collapse.