Coarse-graining support:

Support.Deterministic.CoarseCaccioppoli.EnergyBridge.CenteredLocalCoefficient

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

Centered local coefficient bridge

This module isolates the centered small-cube coefficient bookkeeping used by the descendant Caccioppoli summation. The final scalar comparison is left as a single adequacy hypothesis, while the exact coefficient is reduced to the existing average, Besov, and cutoff-gradient factor bounds.

theorem HCPolySupport.coarseCaccioppoliFluxEnergyExactCenteredCoeff_le_of_separated_factor_bounds {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s C : ℝ) (ξ : Vec d → Vec d) (Acirc1 AcircS B : ℝ) {Aavg AfluxS Xi D A1 AS T : ℝ} (hs0 : 0 < s) (hC : 0 ≤ C) (hB_nonneg : 0 ≤ B) (hAcirc1_nonneg : 0 ≤ Acirc1) (hAcircS_nonneg : 0 ≤ AcircS) (hAavg : √(coarseBBlockNorm Q a) ≤ Aavg) (hAfluxS : (geometricDiscount s 1)⁻¹ * (LambdaSq Q s (MultiscaleExponent.finite 1) a).rpow (1 / 2) ≤ AfluxS) (hξ : cubeLpNorm Q ⊤ ξ ≤ Xi) (hB : B ≤ D) (hAcirc1 : Acirc1 ≤ A1) (hAcircS : AcircS ≤ AS) (hcentered : coarseCaccioppoliFluxEnergyExactCenteredAverageCoeffFactorBound Aavg Xi A1 C + coarseCaccioppoliFluxEnergyExactCenteredBesovCoeffFactorBound Q s Aavg AfluxS (coarseCaccioppoliCenteredCutoffCoeffFactorBound Q s Xi D A1 AS C) ≤ T) : coarseCaccioppoliFluxEnergyExactCenteredCoeff Q a s ξ Acirc1 AcircS B C ≤ T

Centered exact coefficient domination from separated scalar factors.

The hypothesis hcentered is the remaining scalar algebraic comparison against the note-facing centered single-cube coefficient.

theorem HCPolySupport.coarseCaccioppoliCenteredFluxEnergy_le_boundaryCenteredCoefficient {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s C k h : ℝ) (ξ : Vec d → Vec d) (Acirc1 AcircS B : ℝ) {Aavg AfluxS Xi D A1 AS : ℝ} (hs0 : 0 < s) (hC : 0 ≤ C) (hB_nonneg : 0 ≤ B) (hAcirc1_nonneg : 0 ≤ Acirc1) (hAcircS_nonneg : 0 ≤ AcircS) (hAavg : √(coarseBBlockNorm Q a) ≤ Aavg) (hAfluxS : (geometricDiscount s 1)⁻¹ * (LambdaSq Q s (MultiscaleExponent.finite 1) a).rpow (1 / 2) ≤ AfluxS) (hξ : cubeLpNorm Q ⊤ ξ ≤ Xi) (hB : B ≤ D) (hAcirc1 : Acirc1 ≤ A1) (hAcircS : AcircS ≤ AS) (hcentered : coarseCaccioppoliFluxEnergyExactCenteredAverageCoeffFactorBound Aavg Xi A1 C + coarseCaccioppoliFluxEnergyExactCenteredBesovCoeffFactorBound Q s Aavg AfluxS (coarseCaccioppoliCenteredCutoffCoeffFactorBound Q s Xi D A1 AS C) ≤ coarseCaccioppoliSingleCubeBoundaryCenteredCoeff Q a s C k h) : coarseCaccioppoliFluxEnergyExactCenteredCoeff Q a s ξ Acirc1 AcircS B C ≤ coarseCaccioppoliSingleCubeBoundaryCenteredCoeff Q a s C k h

theorem HCPolySupport.coarseCaccioppoliCenteredFluxEnergy_le_local_of_separated_factor {d : ℕ} (R : TriadicCube d) (a : CoeffField d) (s Ceff kR : ℝ) (j : ℕ) (ξ : Vec d → Vec d) (Acirc1 AcircS B : ℝ) {Aavg AfluxS Xi D A1 AS : ℝ} (hs0 : 0 < s) (hCeff : 0 ≤ Ceff) (hB_nonneg : 0 ≤ B) (hAcirc1_nonneg : 0 ≤ Acirc1) (hAcircS_nonneg : 0 ≤ AcircS) (hAavg : √(coarseBBlockNorm R a) ≤ Aavg) (hAfluxS : (geometricDiscount s 1)⁻¹ * (LambdaSq R s (MultiscaleExponent.finite 1) a).rpow (1 / 2) ≤ AfluxS) (hξ : cubeLpNorm R ⊤ ξ ≤ Xi) (hB : B ≤ D) (hAcirc1 : Acirc1 ≤ A1) (hAcircS : AcircS ≤ AS) (hcentered : coarseCaccioppoliFluxEnergyExactCenteredAverageCoeffFactorBound Aavg Xi A1 Ceff + coarseCaccioppoliFluxEnergyExactCenteredBesovCoeffFactorBound R s Aavg AfluxS (coarseCaccioppoliCenteredCutoffCoeffFactorBound R s Xi D A1 AS Ceff) ≤ coarseCaccioppoliSingleCubeBoundaryCenteredCoeff R a s Ceff (kR - ↑j) ↑j) : coarseCaccioppoliFluxEnergyExactCenteredCoeff R a s ξ Acirc1 AcircS B Ceff ≤ coarseCaccioppoliSingleCubeBoundaryCenteredCoeff R a s Ceff (kR - ↑j) ↑j

Local small-cube version of coarseCaccioppoliCenteredFluxEnergy_le_boundaryCenteredCoefficient.

The conclusion has the descendant-local scale kR - j and height j, which is the exact centered branch consumed by the small-cube summation layer.

theorem HCPolySupport.coarseCaccioppoliCenteredFluxEnergy_le_local_boundaryCenteredCoefficient {d : ℕ} (R : TriadicCube d) (a : CoeffField d) (s Ceff kR : ℝ) (j : ℕ) (ξ : Vec d → Vec d) (Acirc1 AcircS B : ℝ) {Xi D A1 AS : ℝ} (hs0 : 0 < s) (hCeff : 0 ≤ Ceff) (hsumS : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale R (R.scale - ↑n) a).rpow (1 / 2)) (hB_nonneg : 0 ≤ B) (hAcirc1_nonneg : 0 ≤ Acirc1) (hAcircS_nonneg : 0 ≤ AcircS) (hξ : cubeLpNorm R ⊤ ξ ≤ Xi) (hB : B ≤ D) (hAcirc1 : Acirc1 ≤ A1) (hAcircS : AcircS ≤ AS) (hcentered : coarseCaccioppoliFluxEnergyExactCenteredAverageCoeffFactorBound (coarseCaccioppoliLambdaFactor R a s) Xi A1 Ceff + coarseCaccioppoliFluxEnergyExactCenteredBesovCoeffFactorBound R s (coarseCaccioppoliLambdaFactor R a s) (coarseCaccioppoliLambdaFactor R a s) (coarseCaccioppoliCenteredCutoffCoeffFactorBound R s Xi D A1 AS Ceff) ≤ coarseCaccioppoliSingleCubeBoundaryCenteredCoeff R a s Ceff (kR - ↑j) ↑j) : coarseCaccioppoliFluxEnergyExactCenteredCoeff R a s ξ Acirc1 AcircS B Ceff ≤ coarseCaccioppoliSingleCubeBoundaryCenteredCoeff R a s Ceff (kR - ↑j) ↑j

Canonical-factor local small-cube centered coefficient bound.

This fills the average and flux slots with coarseCaccioppoliLambdaFactor and uses the descendant cutoff-gradient bound supplied as hξ.

theorem HCPolySupport.coarseCaccioppoliCenteredFluxEnergy_le_local_of_quantitativeCutoff_descendant {d : ℕ} {Q R : TriadicCube d} {j : ℕ} (hR : R ∈ descendantsAtDepth Q j) (a : CoeffField d) (s Ceff kR : ℝ) {ρ₁ ρ₂ : ℝ} (η : QuantitativeCubeCutoff Q ρ₁ ρ₂) (Acirc1 AcircS B : ℝ) {D A1 AS : ℝ} (hs0 : 0 < s) (hCeff : 0 ≤ Ceff) (hsumS : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale R (R.scale - ↑n) a).rpow (1 / 2)) (hB_nonneg : 0 ≤ B) (hB : B ≤ D) (hAcirc1_nonneg : 0 ≤ Acirc1) (hAcircS_nonneg : 0 ≤ AcircS) (hAcirc1 : Acirc1 ≤ A1) (hAcircS : AcircS ≤ AS) (hcentered : coarseCaccioppoliFluxEnergyExactCenteredAverageCoeffFactorBound (coarseCaccioppoliLambdaFactor R a s) (quantitativeCubeCutoffGradientConst d / ((ρ₂ - ρ₁) * cubeRadius Q)) A1 Ceff + coarseCaccioppoliFluxEnergyExactCenteredBesovCoeffFactorBound R s (coarseCaccioppoliLambdaFactor R a s) (coarseCaccioppoliLambdaFactor R a s) (coarseCaccioppoliCenteredCutoffCoeffFactorBound R s (quantitativeCubeCutoffGradientConst d / ((ρ₂ - ρ₁) * cubeRadius Q)) D A1 AS Ceff) ≤ coarseCaccioppoliSingleCubeBoundaryCenteredCoeff R a s Ceff (kR - ↑j) ↑j) : coarseCaccioppoliFluxEnergyExactCenteredCoeff R a s (scalarCutoffGradientField η.toFun) Acirc1 AcircS B Ceff ≤ coarseCaccioppoliSingleCubeBoundaryCenteredCoeff R a s Ceff (kR - ↑j) ↑j

Quantitative parent-cutoff specialization on a depth-j descendant.

The L^\infty bound for the gradient field is supplied by quantitativeCubeCutoff_cubeLpNorm_infty_gradientField_le_on_descendant; the only remaining cutoff-size comparison is the scalar Hessian bound hB.