High-contrast homogenization: Provider.Quenched.UnitRangeNormalizedCutoff #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The normalized local block cutoff #
The one-step ellipticity renormalization is applied after conjugating every local coarse response by the inverse square root of its deterministic annealed mean. This file supplies the locality, integrability, and mean-order facts for the hard whole-block cutoff in those normalized coordinates.
theorem
HCPolySupport.HighContrast.Quenched.measurable_blockMatEntry_normalizedBlock_coarseBlock_standardCell
{d : ℕ}
(F : BlockMat d)
(k : ℤ)
(w : Fin d → ℤ)
(α β : BlockCoord d)
:
Measurable fun (a : CoeffSpace d) => blockMatEntry (normalizedBlock (coarseBlock (standardCell d k w) a) F) α β
The entries of a normalized standard-cell response are measurable for the sigma-field generated by that cell.