High-contrast homogenization: Provider.Quenched.Prop211CellRenormalization

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

Cell-renormalization adapter for the one-time rebase

This file identifies the gain used by the one-time rebase with the gain in the public unit-range cell-renormalization theorem.

theorem HCPolySupport.HighContrast.Quenched.unitRangeCellGain_eq_publicGain (d : ℕ) (g : ℝ) (E : BlockMat d) : unitRangeCellGain d g E = 32 * ↑d ^ 2 * 3 ^ g * frThreshold d * (1 + renormShift d) * kappaRef E

theorem HCPolySupport.HighContrast.Quenched.hasCellRenormalization_unitRangeCellGain_of_frozen {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {g : ℝ} {E : BlockMat d} {Psi : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hstat : IsStationaryLaw P) (hunit : IsUnitRangeLaw P) (hdag : CoarseEllipticityDagger P g E Psi K S) {n l0 h : ℕ} (hl : 0 ≤ ↑n - ↑l0) (hh : h ≤ l0 + 1) (hhalf : (Psi (3 ^ (↑n - ↑l0)))⁻¹ ≤ 1 / 2) : HasCellRenormalization P S (annealedBlock P (centeredCube d (↑n - ↑l0))) g (↑d / 2) (unitRangeCellGain d g E) n l0 h

The public cell-renormalization estimate in the gain convention used by the one-time rebase.