Coarse-graining support:

Support.Deterministic.CoarseCaccioppoli.EnergyBridge.DescendantSummation.Gradient

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.cubeBesovCircPartialNorm_component_le_parent_canonicalGradientAcirc_of_descendant {d : ℕ} {Q R : TriadicCube d} {j : ℕ} (a : CoeffField d) (r : ℝ) (hr : 0 < r) {g : Vec d → Vec d} {energy : Vec d → ℝ} (hR : R ∈ descendantsAtDepth Q j) (henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x) (henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume) (hgrad : CubeAverageGradientEnergyControl Q a g energy) (hsum : Summable fun (n : ℕ) => geometricWeight r 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) (i : Fin d) (N : ℕ) : (cubeBesovCircPartialNorm R r 2 1 N fun (x : Vec d) => g x i) ≤ cubeBesovScaleWeight (-r) Q * ((geometricDiscount r 1)⁻¹ * (lambdaSq Q r (MultiscaleExponent.finite 1) a).rpow (-1 / 2)) * √(cubeAverage R energy)

Descendant-local gradient circ bound with the parent canonical coefficient.

This is the scale-cancellation step in the small-cube proof: the negative scale weight of the descendant cancels the 3^{r j} growth in the localized ellipticity bound.

theorem HCPolySupport.cubeBesovCircPartialNorm_component_le_local_canonicalGradientAcirc {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (r : ℝ) (hr : 0 < r) {g : Vec d → Vec d} {energy : Vec d → ℝ} (henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x) (henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume) (hgrad : CubeAverageGradientEnergyControl Q a g energy) (hsum : Summable fun (n : ℕ) => geometricWeight r 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) (i : Fin d) (N : ℕ) : (cubeBesovCircPartialNorm Q r 2 1 N fun (x : Vec d) => g x i) ≤ cubeBesovScaleWeight (-r) Q * ((geometricDiscount r 1)⁻¹ * (lambdaSq Q r (MultiscaleExponent.finite 1) a).rpow (-1 / 2)) * √(cubeAverage Q energy)

Descendant-local gradient circ bound with the local canonical coefficient.

This is the small-cube version of the gradient-control line in the LaTeX proof: before localization to the parent cube, each descendant keeps its own A^\circ_r(R) factor.

theorem HCPolySupport.local_canonicalGradientAcirc_core_le_parent_of_descendant {d : ℕ} {Q R : TriadicCube d} {j : ℕ} (a : CoeffField d) (r : ℝ) (hr : 0 < r) (hR : R ∈ descendantsAtDepth Q j) (hsum : Summable fun (n : ℕ) => geometricWeight r 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) : cubeBesovScaleWeight (-r) R * ((geometricDiscount r 1)⁻¹ * (lambdaSq R r (MultiscaleExponent.finite 1) a).rpow (-1 / 2)) ≤ cubeBesovScaleWeight (-r) Q * ((geometricDiscount r 1)⁻¹ * (lambdaSq Q r (MultiscaleExponent.finite 1) a).rpow (-1 / 2))

A local canonical gradient A^\circ_r(R) on a depth-j descendant is bounded by the parent canonical factor after the usual descendant scale cancellation.