High-contrast homogenization: Provider.Quenched.SmallContrastEntrySupplySplit

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

The burn-split entry supply at a parametrized normalizer

The free-threshold entry supply at the burn-split frame: the dagger is the enlarged-source datum, the pathwise input is the mesoscale ceiling, and past the burn-in every constant is dimensional — the supply value is (2d)^{1/2}·(κ_𝐄·4)·8·√2, with no boundary constant and no grid-norm power. This is the print's frame discipline (the printed argument, 8446-8455): the geometry rides only in the burn depth, which is a scale threshold.

theorem HCPolySupport.HighContrast.Quenched.entry_lagged_variance_supply_of_block_split {d : ℕ} [NeZero d] (hd : 2 ≤ d) {g : ℝ} (hg : g ∈ Set.Ico 0 1) {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) (hstat : IsStationaryLaw P) {lAl : ℤ} (hl : ↑(kZero d) ≤ lAl) {Cd : ℝ} (hCd : max 1 (12 * ↑d * √↑d) ≤ Cd) {mAl : Mat d} (hn : Matrix.PosDef mAl) (hgrid : IsRoundedGrid lAl (roundedGrid lAl mAl)) {Gacc : ℕ} (hqnorm : ‖roundedGrid lAl mAl‖ * √↑d ≤ 3 ^ Gacc) (hDbc : boundaryConst Cd g mAl ≤ 3 ^ (Gacc + 1)) (hmeso : ∀ᵐ (a : CoeffSpace d) ∂P, ∀ (m : ℤ), S a ≤ 3 ^ m → ∀ k ≤ m, ∀ (w : Fin d → ℤ), standardCellCenter k w ∈ centeredCube d m → BlockMatLoewnerLE (coarseBlock (standardCell d k w) a) (blockScale (3 ^ (g * max (↑m - 2 * ↑(Gacc + 1) - ↑k) 0)) E)) {sKw : ℤ} (hsKw : growthBar K ≤ 3 ^ sKw) {jb p t : ℤ} (hjb : lAl ≤ jb) (hjbp : jb ≤ p) (hpt : p ≤ t) (hsKjb : sKw ≤ jb) (M : ℕ) (hburn : 1 + 2 * ↑(2 + M) * (1 + Real.log (growthBar K)) * growthBar K ^ IndependentSums.natTriangular (2 + M) ≤ 3 ^ (↑M * ↑(jb + ↑(Gacc + 1) - 1 - sKw))) (hsmjb : ↑d * (adaptedHattedContrast P (roundedGrid lAl mAl) jb - 1) ≤ 1 / 2) (hsmp : ↑d * (adaptedHattedContrast P (roundedGrid lAl mAl) p - 1) ≤ 1 / 2) (hdropB : 4 * ↑d * (adaptedHattedContrast P (roundedGrid lAl mAl) jb - adaptedHattedContrast P (roundedGrid lAl mAl) t) ≤ 1) {F : BlockMat d} (hFsym : IsSymmetricBlockMat F) (hFpd : Book.Ch02.BlockPosDef F) (henvF : BlockMatLoewnerLE (adaptedMean P (roundedGrid lAl mAl) p) F) {Csub : ℝ} (hCsub : 0 < Csub) (hsubdiv : ∀ (j' p' : ℤ), lAl ≤ j' → j' ≤ p' → ∃ (Z : Finset (Fin d → ℤ)), ↑Z = {w : Fin d → ℤ | adaptedCellCenter (roundedGrid lAl mAl) j' w ∈ adaptedCell (roundedGrid lAl mAl) p'} ∧ Z.card = 3 ^ (d * (p' - j').toNat) ∧ Z.Nonempty ∧ lqSchattenSize P 2 (fun (a : CoeffSpace d) => blockSub (ofFullBlockMat ((↑Z.card)⁻¹ • ∑ w ∈ Z, toFullBlockMat (coarseBlock (adaptedCellAt (roundedGrid lAl mAl) j' w) a))) (adaptedMean P (roundedGrid lAl mAl) j')) (adaptedMean P (roundedGrid lAl mAl) p') ≤ ENNReal.ofReal (Csub * ↑Z.card ^ (-2⁻¹)) * lqSchattenSize P 2 (fun (a : CoeffSpace d) => blockSub (coarseBlock (adaptedCell (roundedGrid lAl mAl) j') a) (adaptedMean P (roundedGrid lAl mAl) j')) (adaptedMean P (roundedGrid lAl mAl) p')) : scaleVariance P (roundedGrid lAl mAl) F p ≤ ENNReal.ofReal (√(2 * ↑d) * 1 * ((2 + 4 * (1 + 4 * ↑d * (adaptedHattedContrast P (roundedGrid lAl mAl) jb - adaptedHattedContrast P (roundedGrid lAl mAl) p)) ^ 2) * (Csub * ↑(3 ^ (d * (p - jb).toNat)) ^ (-2⁻¹) * ((2 * ↑d) ^ 2⁻¹ * (kappaRef E * 4) * (2 * 4) * √2)) + 4 * (1 + 4 * ↑d * (adaptedHattedContrast P (roundedGrid lAl mAl) jb - adaptedHattedContrast P (roundedGrid lAl mAl) p)) ^ 2 * (36 * (↑d * (adaptedHattedContrast P (roundedGrid lAl mAl) jb - 1) + 1 / 2 * 3 ^ (-↑(p - jb).toNat))) + 4 * ↑d * (adaptedHattedContrast P (roundedGrid lAl mAl) jb - adaptedHattedContrast P (roundedGrid lAl mAl) p)))

The burn-split entry supply.