Coarse-graining support:

Support.Deterministic.CoarseCaccioppoli.EnergyBridge.DescendantSummation.Averages

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.abs_cubeAverage_le_descendantsAverage_abs_cubeAverage_of_integrableOn {d : ℕ} (Q : TriadicCube d) (j : ℕ) (f : Vec d → ℝ) (hf : MeasureTheory.IntegrableOn f (cubeSet Q) MeasureTheory.volume) : |cubeAverage Q f| ≤ descendantsAverage Q j fun (R : TriadicCube d) => |cubeAverage R f|

Triangle inequality after decomposing a cube average into depth-j descendant cube averages.

theorem HCPolySupport.abs_cubeAverage_le_descendantsAverage_of_local_abs_bounds {d : ℕ} (Q : TriadicCube d) (j : ℕ) (f : Vec d → ℝ) (B : TriadicCube d → ℝ) (hf : MeasureTheory.IntegrableOn f (cubeSet Q) MeasureTheory.volume) (hlocal : ∀ R ∈ descendantsAtDepth Q j, |cubeAverage R f| ≤ B R) : |cubeAverage Q f| ≤ descendantsAverage Q j B

If each depth-j descendant cube average is bounded by a local RHS, then the parent cube average is bounded by the descendants-average of those local RHS values.

theorem HCPolySupport.abs_cubeAverage_vecDot_scalar_smul_le_descendantsAverage_of_local_bounds {d : ℕ} (Q : TriadicCube d) (j : ℕ) (flux ξ : Vec d → Vec d) (u : Vec d → ℝ) (B : TriadicCube d → ℝ) (hf : MeasureTheory.IntegrableOn (fun (x : Vec d) => vecDot (flux x) (u x • ξ x)) (cubeSet Q) MeasureTheory.volume) (hlocal : ∀ R ∈ descendantsAtDepth Q j, |cubeAverage R fun (x : Vec d) => vecDot (flux x) (u x • ξ x)| ≤ B R) : |cubeAverage Q fun (x : Vec d) => vecDot (flux x) (u x • ξ x)| ≤ descendantsAverage Q j B

Descendant summation specialized to the Caccioppoli cutoff pairing. The local estimates may come from any source, in particular from abs_cubeAverage_vectorDot_scalarMultiply_le_singleCubeBoundaryNoteRhs.

theorem HCPolySupport.cubeAverage_vectorDot_scalarMultiply_scalarCutoffGradientField_eq_zero {d : ℕ} {Q R : TriadicCube d} {ρ₁ ρ₂ : ℝ} (η : QuantitativeCubeCutoff Q ρ₁ ρ₂) (flux : Vec d → Vec d) (u : Vec d → ℝ) (hout : ∀ x ∈ cubeSet R, x ∉ scaledClosedCubeSet Q ρ₂) : (cubeAverage R fun (x : Vec d) => vecDot (flux x) (u x • scalarCutoffGradientField η.toFun x)) = 0

If a cube lies outside the outer support of a quantitative cutoff, then the local cutoff-gradient flux pairing over that cube is zero.

theorem HCPolySupport.descendantsAverage_add_local {d : ℕ} (Q : TriadicCube d) (j : ℕ) (F G : TriadicCube d → ℝ) : (descendantsAverage Q j fun (R : TriadicCube d) => F R + G R) = descendantsAverage Q j F + descendantsAverage Q j G

theorem HCPolySupport.descendantsAverage_const_local {d : ℕ} (Q : TriadicCube d) (j : ℕ) (c : ℝ) : (descendantsAverage Q j fun (x : TriadicCube d) => c) = c

theorem HCPolySupport.descendantsAverage_sqrt_le_sqrt_descendantsAverage_of_nonneg {d : ℕ} (Q : TriadicCube d) (j : ℕ) (F : TriadicCube d → ℝ) (hF : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ F R) : (descendantsAverage Q j fun (R : TriadicCube d) => √(F R)) ≤ √(descendantsAverage Q j F)

Jensen/Cauchy for the finite descendant average: the average of square roots is controlled by the square root of the average.

theorem HCPolySupport.descendantsAverage_cubeLpNorm_two_mul_sqrt_cubeAverage_le {d : ℕ} (Q : TriadicCube d) (j : ℕ) (u energy : Vec d → ℝ) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x) (henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume) : (descendantsAverage Q j fun (R : TriadicCube d) => cubeLpNorm R 2 u * √(cubeAverage R energy)) ≤ cubeLpNorm Q 2 u * √(cubeAverage Q energy)

Descendant Cauchy estimate for the constant branch of the small-cube Caccioppoli proof.

This is the step that lets the proof use the parent normalized L² norm of u after summing over descendants, instead of requiring a pointwise L² bound on every small cube.

theorem HCPolySupport.descendantsAverage_cubeAverage_indicator_scaledClosedCubeSet_eq_localizedEnergyProfile {d : ℕ} (Q : TriadicCube d) (j : ℕ) (ρ : ℝ) (energy : Vec d → ℝ) (henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume) : (descendantsAverage Q j fun (R : TriadicCube d) => cubeAverage R ((scaledClosedCubeSet Q ρ).indicator energy)) = coarseCaccioppoliLocalizedEnergyProfile Q ρ energy

Descendant averages of the outer-localized energy density collapse to the outer localized parent profile, not to the full-cube energy average.

theorem HCPolySupport.descendantsAverage_cubeLpNorm_two_mul_sqrt_cubeAverage_indicator_scaledClosedCubeSet_le {d : ℕ} (Q : TriadicCube d) (j : ℕ) (ρ : ℝ) (u energy : Vec d → ℝ) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x) (henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume) : (descendantsAverage Q j fun (R : TriadicCube d) => cubeLpNorm R 2 u * √(cubeAverage R ((scaledClosedCubeSet Q ρ).indicator energy))) ≤ cubeLpNorm Q 2 u * √(coarseCaccioppoliLocalizedEnergyProfile Q ρ energy)

Finite Cauchy for the constant branch after replacing the energy density by its outer-localized version. This is the summation shape needed by the localized raw Caccioppoli repair.

theorem HCPolySupport.descendantsAverage_cubeAverage_indicator_coarseCaccioppoliLocalClosedCube_eq_localEnergyProfile {d : ℕ} (Q : TriadicCube d) (center : Vec d) (j : ℕ) (rho : ℝ) (energy : Vec d → ℝ) (henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume) : (descendantsAverage Q j fun (R : TriadicCube d) => cubeAverage R ((coarseCaccioppoliLocalClosedCube Q center rho).indicator energy)) = coarseCaccioppoliLocalEnergyProfile Q center rho energy

Descendant averages of the arbitrary-center local-patch energy density collapse to the corresponding local parent profile.

theorem HCPolySupport.descendantsAverage_L2Norm_sqrtLocalEnergy_le_parentProduct {d : ℕ} (Q : TriadicCube d) (center : Vec d) (j : ℕ) (rho : ℝ) (u energy : Vec d → ℝ) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x) (henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume) : (descendantsAverage Q j fun (R : TriadicCube d) => cubeLpNorm R 2 u * √(cubeAverage R ((coarseCaccioppoliLocalClosedCube Q center rho).indicator energy))) ≤ cubeLpNorm Q 2 u * √(coarseCaccioppoliLocalEnergyProfile Q center rho energy)

Finite Cauchy for the constant branch after replacing the energy density by the arbitrary-center local-patch localization.