High-contrast homogenization: Provider.Quenched.SmallContrastVarianceLagged #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The lagged variance measurability and average carrier #
Measurability of the subdivision-average fluctuation size against an arbitrary positive frame, by the entrywise route, and its identification with the norm of the normalized block.
theorem
HCPolySupport.HighContrast.Quenched.aemeasurable_blockSize_subdivisionDefect
{d : ℕ}
{P : MeasureTheory.Measure (CoeffSpace d)}
{q : Mat d}
(hq : Matrix.PosDef q)
(j : ℤ)
(Z : Finset (Fin d → ℤ))
{Gj Gp : BlockMat d}
(hGjsym : IsSymmetricBlockMat Gj)
(hGpsym : IsSymmetricBlockMat Gp)
(hGppd : Book.Ch02.BlockPosDef Gp)
:
AEMeasurable
(fun (a : CoeffSpace d) =>
blockSize
(blockSub (ofFullBlockMat ((↑Z.card)⁻¹ • ∑ w ∈ Z, toFullBlockMat (coarseBlock (adaptedCellAt q j w) a))) Gj) Gp)
P
Measurability of the subdivision-average fluctuation size.