High-contrast homogenization: Provider.Quenched.SmallContrastVarianceCore

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

The abstract variance split

The pathwise chain of Lemma 4.4 of HC as a pure matrix estimate: a positive parent below the average of positive children, dominating its sharp, has normalized distance to the terminal frame controlled by the children's average fluctuation around the intermediate frame plus the sharp-gap and dilation terms. All anchors are abstract, so the estimate applies unchanged at the recentered (hatted) objects, where the two frame-sensitive scalar inputs are dischargeable.

theorem HCPolySupport.HighContrast.Quenched.norm_normalized_parent_fluctuation_le {d : ℕ} {ι : Type u_1} (Z : Finset ι) (hZne : Z.Nonempty) (A : ι → FullBlockMat d) (hA : ∀ i ∈ Z, Matrix.PosDef (A i)) {Ap Gj Gp : FullBlockMat d} (hAp : Matrix.PosDef Ap) (hGj : Matrix.PosDef Gj) (hGp : Matrix.PosDef Gp) (hparentLe : Ap ≤ (↑Z.card)⁻¹ • ∑ i ∈ Z, A i) (hparentSharp : fullBlockSharp Ap ≤ Ap) (hsharpJle : fullBlockSharp Gj ≤ Gj) (horder : Gp ≤ Gj) {cH cJ cD : ℝ} (hcH0 : 0 ≤ cH) (hcJ0 : 0 ≤ cJ) (hcD0 : 0 ≤ cD) (hsharpPinv : (fullBlockSharp Gp)⁻¹ ≤ cH • Gp⁻¹) (hgapJ : Gj - fullBlockSharp Gj ≤ cJ • Gp) (hdil : Gj ≤ (1 + cD) • Gp) : ‖matSqrt Gp⁻¹ * (Ap - Gp) * matSqrt Gp⁻¹‖ ≤ (2 + cH * (1 + cD) ^ 2) * ‖matSqrt Gp⁻¹ * ((↑Z.card)⁻¹ • ∑ i ∈ Z, A i - Gj) * matSqrt Gp⁻¹‖ + cH * (1 + cD) ^ 2 * cJ + cD

The abstract pathwise variance split.