Coarse-graining support: Support.Deterministic.CoarseCaccioppoli.EnergyBridge.LocalConstantBranch

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

Local constant branch coefficient helpers

This file isolates the bounded coefficient step for the constant branch in the small-cube Caccioppoli route. The local L² norm of u has already been factored out by the descendant summation argument, so the target is the single-cube base coefficient.

theorem HCPolySupport.coarseCaccioppoliConstantFluxEnergy_le_boundaryCoefficient_of_factorBounds {d : ℕ} (R : TriadicCube d) (a : CoeffField d) (ξ : Vec d → Vec d) {B Ceff kR Aavg Aflux1 Xi : ℝ} (j : ℕ) (hB_nonneg : 0 ≤ B) (hAavg : √(coarseBBlockNorm R a) ≤ Aavg) (hAflux1 : (geometricDiscount 1 1)⁻¹ * (LambdaSq R 1 (MultiscaleExponent.finite 1) a).rpow (1 / 2) ≤ Aflux1) (hξ : cubeLpNorm R ⊤ ξ ≤ Xi) (hbounded : coarseCaccioppoliFluxEnergyExactConstantCoeffFactorBound R Aavg Aflux1 * (B + cubeBesovScaleWeight 1 R * Xi) ≤ coarseCaccioppoliSingleCubeBoundaryConstantBaseCoeff R a Ceff (kR - ↑j)) : coarseCaccioppoliFluxEnergyExactConstantCoeff R a * (B + cubeBesovScaleWeight 1 R * cubeLpNorm R ⊤ ξ) ≤ coarseCaccioppoliSingleCubeBoundaryConstantBaseCoeff R a Ceff (kR - ↑j)

Constant-branch local coefficient comparison from separated coefficient factor bounds and an L∞ bound for the cutoff gradient.

The final scalar hypothesis is the remaining deterministic adequacy comparison between the bounded exact coefficient/cutoff expression and the local single-cube base coefficient at scale kR - j.

theorem HCPolySupport.coarseCaccioppoliConstantFluxEnergy_le_boundaryCoefficient_of_cutoffGradient {d : ℕ} {Q R : TriadicCube d} {j : ℕ} (hR : R ∈ descendantsAtDepth Q j) (a : CoeffField d) {ρ₁ ρ₂ : ℝ} (η : QuantitativeCubeCutoff Q ρ₁ ρ₂) {B Ceff kR Aavg Aflux1 : ℝ} (hB_nonneg : 0 ≤ B) (hAavg : √(coarseBBlockNorm R a) ≤ Aavg) (hAflux1 : (geometricDiscount 1 1)⁻¹ * (LambdaSq R 1 (MultiscaleExponent.finite 1) a).rpow (1 / 2) ≤ Aflux1) (hbounded : coarseCaccioppoliFluxEnergyExactConstantCoeffFactorBound R Aavg Aflux1 * (B + cubeBesovScaleWeight 1 R * (quantitativeCubeCutoffGradientConst d / ((ρ₂ - ρ₁) * cubeRadius Q))) ≤ coarseCaccioppoliSingleCubeBoundaryConstantBaseCoeff R a Ceff (kR - ↑j)) : coarseCaccioppoliFluxEnergyExactConstantCoeff R a * (B + cubeBesovScaleWeight 1 R * cubeLpNorm R ⊤ (scalarCutoffGradientField η.toFun)) ≤ coarseCaccioppoliSingleCubeBoundaryConstantBaseCoeff R a Ceff (kR - ↑j)

Descendant version for a parent quantitative cutoff. The L∞ cutoff gradient input is supplied by the standard descendant-local quantitative cutoff bound.