Coarse-graining support: Support.Book.Ch03.Theorems.PublicInternalBridges.CoarseGrainingL2

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

Public/internal coarse-graining L2 RHS bridge

This file contains the terminal dimension-loss comparison for the deterministic coarse-graining L2 RHS written with the Chapter 3 public coefficient field.

Audit tag

Claim: the deterministic public-coefficient coarse-graining L2 RHS is bounded by the Chapter 3 public RHS after the explicit dimension-square loss.

Downstream target: the scale-separated Ch3 aggregate theorem surface. This file is bridge plumbing only and introduces no public *Theory package.

theorem HCPolySupport.Book.Ch03.coarseGrainingFluxBoundTwoExponent_le_dim_sq_mul {d : ℕ} [NeZero d] (C : ℝ) (Q : TriadicCube d) (a : CoeffFamily d) (a0 : ConstantCoeffMatrix d) {s t : ℝ} (j : ℕ) {g : Vec d → Vec d} (u : H1Function (Ch02.cubeDomain Q).carrier) (hC : 0 ≤ C) (hs : 0 < s) (hB_nonneg : 0 ≤ cubeBesovPositiveVectorSeminormTwo Q t g) (hH_nonneg : 0 ≤ coarseGrainingHomogenizationErrorAtDepth Q a a0 s j) (herror : HCPolySupport.coarseGrainingHomogenizationErrorAtDepth Q (publicCoeffField Q a) a0.matrix s j = coarseGrainingHomogenizationErrorAtDepth Q a a0 s j) : C * coarseGrainingL2FluxDefectBoundTwoExponent Q (publicCoeffField Q a) a0.matrix s t j u.grad g ≤ generalCoarseGrainingL2TwoExponentFluxDefectRHS (↑d ^ 2 * C) Q a a0 s t j g u

Scale-separated flux-defect version of the public/internal coarse-graining RHS bridge.