High-contrast homogenization: Provider.Quenched.SmallContrastVarianceFrames #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The frame inputs of the variance split #
The two frame-sensitive scalar inputs of the abstract variance split, discharged at the recentered means: the terminal recentered mean is within factor four of its sharp, and the lower-scale recentered sharp gap is first order in the hatted contrast defect, both against the terminal frame. The recentering is at the lower scale's response skew, so the symmetric parts are controlled by the smallness packs and the skew difference by the good quadratics.
theorem
HCPolySupport.HighContrast.Quenched.hatted_sharp_inverse_bound
{d : ℕ}
{Sp SStarp Kp : Mat d}
(hSp : Matrix.PosDef Sp)
(hStarp : Matrix.PosDef SStarp)
{epsp : ℝ}
(hposp : 0 ≤ epsp)
(hepsp1 : epsp ≤ 1)
(hgapMp : Sp - SStarp ≤ epsp • SStarp)
(hskewMp : Response.responseSymmetric Kp * SStarp⁻¹ * Response.responseSymmetric Kp ≤ (epsp ^ 2 / 4) • SStarp)
(h0 : Mat d)
(hh0 : IsSkewMat h0)
:
The terminal recentered sharp comparison with constant four.
theorem
HCPolySupport.HighContrast.Quenched.hatted_sharp_gap_bound
{d : ℕ}
{Sj SStarj : Mat d}
(hSj : Matrix.PosDef Sj)
(hStarj : Matrix.PosDef SStarj)
{epsj : ℝ}
(hposj : 0 ≤ epsj)
(hepsj1 : epsj ≤ 1)
(horderj : SStarj ≤ Sj)
(hgapMj : Sj - SStarj ≤ epsj • SStarj)
{κ : Mat d}
(hκ : Matrix.conjTranspose κ = κ)
(hskewMj : κ * SStarj⁻¹ * κ ≤ (epsj ^ 2 / 4) • SStarj)
{Sp SStarp Khatp : Mat d}
(hSp : Matrix.PosDef Sp)
(hStarp : Matrix.PosDef SStarp)
(horderp : SStarp ≤ Sp)
(hstarcross : SStarj ≤ SStarp)
(hdilquad : ∀ (y : Vec d), y ⬝ᵥ SStarj⁻¹.mulVec y ≤ 2 * y ⬝ᵥ SStarp⁻¹.mulVec y)
(hKhat : ∀ (x : Vec d), Matrix.mulVec Khatp x ⬝ᵥ SStarp⁻¹.mulVec (Matrix.mulVec Khatp x) ≤ x ⬝ᵥ Matrix.mulVec Sp x)
:
schurBlock Sj SStarj κ - fullBlockSharp (schurBlock Sj SStarj κ) ≤ (36 * epsj) • schurBlock Sp SStarp Khatp
The lower-scale recentered sharp gap is first order in the smallness parameter against the terminal frame.