High-contrast homogenization: Provider.Quenched.SmallContrastLoadQuads

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

The calibrated load quadratics

The two Schur-form quadratics of the recentered terminal mean at the calibrated load pair (-p, r) (and its adjoint mirror (p, r)) are bounded by the absolute constant 7 under the smallness pack, and the skew-shifted load pairings are exactly one. These are the only load-dependent factors of the weak-cap majorant, so the weak value becomes uniform over unit directions.

theorem HCPolySupport.HighContrast.Quenched.calibrated_load_quads_le {d : ℕ} {S SStar κ : Mat d} (hS : Matrix.PosDef S) (hStar : Matrix.PosDef SStar) (hκ : Matrix.conjTranspose κ = κ) {eps : ℝ} (heps0 : 0 ≤ eps) (heps1 : eps ≤ 1) (horder : SStar ≤ S) (hgapM : S - SStar ≤ eps • SStar) (hskewM : κ * SStar⁻¹ * κ ≤ (eps ^ 2 / 4) • SStar) (e : Vec d) (he : e ⬝ᵥ e = 1) : (matSqrt (matGeomMean (S + κ * SStar⁻¹ * κ) SStar)⁻¹).mulVec e ⬝ᵥ Matrix.mulVec S ((matSqrt (matGeomMean (S + κ * SStar⁻¹ * κ) SStar)⁻¹).mulVec e) + ((matSqrt (matGeomMean (S + κ * SStar⁻¹ * κ) SStar)).mulVec e + Matrix.mulVec κ ((matSqrt (matGeomMean (S + κ * SStar⁻¹ * κ) SStar)⁻¹).mulVec e)) ⬝ᵥ SStar⁻¹.mulVec ((matSqrt (matGeomMean (S + κ * SStar⁻¹ * κ) SStar)).mulVec e + Matrix.mulVec κ ((matSqrt (matGeomMean (S + κ * SStar⁻¹ * κ) SStar)⁻¹).mulVec e)) ≤ 7 ∧ (matSqrt (matGeomMean (S + κ * SStar⁻¹ * κ) SStar)⁻¹).mulVec e ⬝ᵥ Matrix.mulVec S ((matSqrt (matGeomMean (S + κ * SStar⁻¹ * κ) SStar)⁻¹).mulVec e) + ((matSqrt (matGeomMean (S + κ * SStar⁻¹ * κ) SStar)).mulVec e - Matrix.mulVec κ ((matSqrt (matGeomMean (S + κ * SStar⁻¹ * κ) SStar)⁻¹).mulVec e)) ⬝ᵥ SStar⁻¹.mulVec ((matSqrt (matGeomMean (S + κ * SStar⁻¹ * κ) SStar)).mulVec e - Matrix.mulVec κ ((matSqrt (matGeomMean (S + κ * SStar⁻¹ * κ) SStar)⁻¹).mulVec e)) ≤ 7

The two hatted load quadratics are at most 7.

theorem HCPolySupport.HighContrast.Quenched.calibrated_pair_skew_abs {d : ℕ} {b SStar : Mat d} (hb : Matrix.PosDef b) (hStar : Matrix.PosDef SStar) {h0 : Mat d} (hh0 : IsSkewMat h0) (e : Vec d) (he : e ⬝ᵥ e = 1) : |(matSqrt (matGeomMean b SStar)⁻¹).mulVec e ⬝ᵥ ((matSqrt (matGeomMean b SStar)).mulVec e - Matrix.mulVec h0 ((matSqrt (matGeomMean b SStar)⁻¹).mulVec e))| = 1 ∧ |(matSqrt (matGeomMean b SStar)⁻¹).mulVec e ⬝ᵥ ((matSqrt (matGeomMean b SStar)).mulVec e + Matrix.mulVec h0 ((matSqrt (matGeomMean b SStar)⁻¹).mulVec e))| = 1

The skew-shifted load pairings are exactly one.

theorem HCPolySupport.HighContrast.Quenched.hatMean_blockQuad_eq {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {q : Mat d} (t : ℤ) {S SStar K : Mat d} (hform : toFullBlockMat (adaptedMean P q t) = schurBlock S SStar K) (x y : Vec d) : blockVecDot (x, y) (blockMatVecMul (Response.skewBlockCongr (Response.responseSkew K) (adaptedMean P q t)) (x, y)) = x ⬝ᵥ Matrix.mulVec S x + (y - Matrix.mulVec (Response.responseSymmetric K) x) ⬝ᵥ SStar⁻¹.mulVec (y - Matrix.mulVec (Response.responseSymmetric K) x)

The recentered hatted mean quadratic in closed Schur form.