High-contrast homogenization: Provider.Quenched.SmallContrastCenterVariance

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

The centering variance by the terminal single-cell variance

The annealed-centering variance of the weak state — the third group of the weak-root majorant — is bounded by the terminal single-cell fluctuation carrier: the cell average of the weak state is an affine function of the pathwise coarse block (the all-averages identity), so its fluctuation around the annealed center is Lipschitz in the fluctuation of the coarse block around the adapted mean. No portable history enters.

theorem HCPolySupport.HighContrast.Quenched.profilePrimalCenterVariance_le_variance {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {m : Mat d} (hm : Matrix.PosDef m) {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (hint : HasFiniteAdaptedMean P q t) (hEt : Book.Ch02.BlockPosDef (adaptedMean P q t)) (h0 : Mat d) (hh0 : IsSkewMat h0) (p r : Vec d) : Response.profilePrimalCenterVariance P m hq t (fun (a : CoeffSpace d) => a.subSkew h0 hh0) p r ≤ ENNReal.ofReal (Response.diagonalWeakMetricFactor m (Response.skewBlockCongr h0 (adaptedMean P q t)) * Response.diagonalWeakLoadMinus (Response.skewBlockCongr h0 (adaptedMean P q t)) p r) * scaleVariance P q (adaptedMean P q t) t

The centering variance at the recentered samples is bounded by the terminal single-cell fluctuation carrier in the adapted-mean normalization.