High-contrast homogenization: Provider.Quenched.SmallContrastWeakAverageVariance

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

The recent average sums by per-scale variances

The weighted recent average sum of the weak-norm split is bounded in L²(P) by the square roots of the same per-scale variance carriers and mean drops: the normalized average defect is dominated pathwise by the average of the per-cell normalized deviations (the operator norm of an average is at most the average of the norms), whose first moments are the per-scale carriers by the exponent comparison on the probability space. This is the second (aligned average) group of the printed display HC (3.68).

theorem HCPolySupport.HighContrast.Quenched.aemeasurable_blockSize_averageDefect {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {q : Mat d} (hq : Matrix.PosDef q) (k t : ℤ) (F : BlockMat d) : AEMeasurable (fun (a : CoeffSpace d) => blockSize (Response.diagonalWeakAverageDefect q k t F a) (Book.Ch02.blockIdentity d)) P

Measurability of the identity-size of the average defect at an arbitrary normalization.