High-contrast homogenization: Provider.Quenched.UnitRangeRenormalizedFamily

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

The renormalized minimal scales as a generation-indexed family

The endgame replays the renormalization of ellipticity once for every base generation, against a reference block that changes with the generation, and feeds the resulting family of minimal scales to the bad-tail engine. This file records the family, the existence of the buffer that absorbs the union-bound prefactor, the deterministic conclusion below a minimal scale, and the composition with the engine.

The tail constant is c_fr(d) throughout: it is fixed before the exponent and before every datum of the law.

The buffer

The deterministic conclusion below the minimal scale

theorem HCPolySupport.HighContrast.Quenched.blockMatLoewnerLE_of_renormRadius_le {d : ℕ} {S : CoeffSpace d → ℝ} {Ahat : BlockMat d} {delta rho : ℝ} {h n : ℕ} {a : CoeffSpace d} {m : ℤ} (hfin : renormScale S Ahat delta rho h n a ≠ ⊤) (hnm : ↑n ≤ m) (hle : renormRadius S Ahat delta rho h n a ≤ 3 ^ m) (hsrc : S a ≤ 3 ^ m) (k : ℤ) : m - ↑h + 1 ≤ k → k ≤ m → ∀ (w : Fin d → ℤ), standardCellCenter k w ∈ centeredCube d m → BlockMatLoewnerLE (coarseBlock (standardCell d k w) a) (blockScale (1 + delta * 3 ^ (rho * (↑m - ↑k))) Ahat)

The window range of the renormalized ellipticity conclusion. Below the minimal scale of the base generation, and on the event that the source has burnt in, every cell of every scale in the window obeys the additive comparison with the reference block.

The family and the engine composition