Coarse-graining support:

Support.Deterministic.CoarseCaccioppoli.SingleCubeToRaw.HarmonicFinal.ExactSmallCube .CenteredFactors.LocalAlpha

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

Exact small-cube centered factors: local alpha comparison

theorem HCPolySupport.coarseCaccioppoliFluxEnergyExactCenteredBesovCoeffFactorBound_localAcirc_le_alpha_of_scale {d : ℕ} [NeZero d] {Q R : TriadicCube d} (a : CoeffField d) {s t CeffLocal CeffWork : ℝ} {k j : ℕ} {ρ₁ ρ₂ lam Lam : ℝ} {hheight : ℝ → ℝ → ℝ} (hCeffLocal : 0 ≤ CeffLocal) (hCeffWork : 0 ≤ CeffWork) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hEllCube : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hR : R ∈ descendantsAtDepth Q j) (hBsum_s : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) (hSigmaSum_t : Summable fun (n : ℕ) => geometricWeight t 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) (hchoice : CoarseCaccioppoliTriadicGapScaleChoice k ρ₁ ρ₂) (hlt : ρ₁ < ρ₂) (hjk : k ≤ j) (hscale : (coarseCaccioppoliCenteredBesovHessianFront d s CeffLocal + coarseCaccioppoliCenteredBesovGradientFront d s CeffLocal) * Real.rpow 3 ↑k ≤ CeffWork / (s * (1 - s)) * coarseCaccioppoliGapInv ρ₁ ρ₂) (hheight_le_j : hheight ρ₁ ρ₂ ≤ ↑j) : coarseCaccioppoliFluxEnergyExactCenteredBesovCoeffFactorBound R s (coarseCaccioppoliLambdaFactor R a s) (coarseCaccioppoliLambdaFactor R a s) (coarseCaccioppoliCenteredCutoffCoeffFactorBound R s (coarseCaccioppoliQuantitativeCutoffGradientBound Q ρ₁ ρ₂) (coarseCaccioppoliQuantitativeCutoffHessianBound Q ρ₁ ρ₂) (coarseCaccioppoliCanonicalGradientAcircOne R a ρ₁ ρ₂) (coarseCaccioppoliCanonicalGradientAcircOneSub R a s ρ₁ ρ₂) CeffLocal) ≤ coarseCaccioppoliBoundaryAlphaOfHeight Q a s t CeffWork hheight ρ₁ ρ₂

The Besov/cutoff-product part of the centered exact coefficient localizes to the parent Alpha coefficient once the two Besov scalar fronts are absorbed into the working constant. This is the second substitution line in the LaTeX centered single-cube estimate: the Hessian and gradient cutoff gains are estimated separately, but both descendant ellipticity products are compared to the same parent theta term.

theorem HCPolySupport.coarseCaccioppoliFluxEnergyExactCenteredFactorBounds_localAcirc_le_alpha_of_scale {d : ℕ} [NeZero d] {Q R : TriadicCube d} (a : CoeffField d) {s t CeffLocal CeffWork : ℝ} {k j : ℕ} {ρ₁ ρ₂ lam Lam : ℝ} {hheight : ℝ → ℝ → ℝ} (hCeffLocal : 0 ≤ CeffLocal) (hCeffWork : 0 ≤ CeffWork) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hEllCube : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hR : R ∈ descendantsAtDepth Q j) (hBsum_s : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) (hSigmaSum_t : Summable fun (n : ℕ) => geometricWeight t 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) (hchoice : CoarseCaccioppoliTriadicGapScaleChoice k ρ₁ ρ₂) (hlt : ρ₁ < ρ₂) (hjk : k ≤ j) (hscale : (coarseCaccioppoliCenteredAverageFront d s CeffLocal + coarseCaccioppoliCenteredBesovHessianFront d s CeffLocal + coarseCaccioppoliCenteredBesovGradientFront d s CeffLocal) * Real.rpow 3 ↑k ≤ CeffWork / (s * (1 - s)) * coarseCaccioppoliGapInv ρ₁ ρ₂) (hheight_le_j : hheight ρ₁ ρ₂ ≤ ↑j) : coarseCaccioppoliFluxEnergyExactCenteredAverageCoeffFactorBound (coarseCaccioppoliLambdaFactor R a s) (coarseCaccioppoliQuantitativeCutoffGradientBound Q ρ₁ ρ₂) (coarseCaccioppoliCanonicalGradientAcircOne R a ρ₁ ρ₂) CeffLocal + coarseCaccioppoliFluxEnergyExactCenteredBesovCoeffFactorBound R s (coarseCaccioppoliLambdaFactor R a s) (coarseCaccioppoliLambdaFactor R a s) (coarseCaccioppoliCenteredCutoffCoeffFactorBound R s (coarseCaccioppoliQuantitativeCutoffGradientBound Q ρ₁ ρ₂) (coarseCaccioppoliQuantitativeCutoffHessianBound Q ρ₁ ρ₂) (coarseCaccioppoliCanonicalGradientAcircOne R a ρ₁ ρ₂) (coarseCaccioppoliCanonicalGradientAcircOneSub R a s ρ₁ ρ₂) CeffLocal) ≤ coarseCaccioppoliBoundaryAlphaOfHeight Q a s t CeffWork hheight ρ₁ ρ₂

The average and Besov factor-bound pieces of the centered exact coefficient localize together to one parent Alpha coefficient. This is the combined budget line in the LaTeX proof: the average front, Hessian front, and gradient front are absorbed by a single work-constant inequality before applying the height monotonicity of Alpha.