High-contrast homogenization: Provider.Quenched.SmallContrastMetricFactorTau

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

The shear size of the response skew

The recentering skew of the small-contrast weak norm is h_0 = h_rsp(K_t), the antisymmetric part of the Schur skew coordinate of the terminal adapted mean. The metric factor of SmallContrastMetricFactor needs the m_0-normalized size τ of this skew, and it must not grow with the generation.

The bound is read off a two-sided comparison of the terminal mean with the split metric M_0 = diag(m_0,m_0^{-1}):

• the upper half, at the doubled vector (x,0), gives |σ_*^{-1/2}K x|² ≤ C |m_0^{1/2}x|² — the Schur form's own (0 - Kx) slot;
• the lower half, at (0,y), gives |m_0^{-1/2}y|² ≤ κ |σ_*^{-1/2}y|²;

and reading the second at y = Kx produces |m_0^{-1/2}Kx|² ≤ κ C |m_0^{1/2}x|², i.e. the normalized Schur coordinate has size at most (κC)^{1/2}.

The passage from K to its antisymmetric part costs nothing: the transposed bound follows from the same one by Cauchy–Schwarz in the m_0 metric, and the parallelogram bound absorbs the factor 1/2 of the antisymmetrization.

Elementary facts about a positive quadratic form

The transposed bound

theorem HCPolySupport.HighContrast.Quenched.quad_transpose_le {d : ℕ} {m K : Mat d} (hm : Matrix.PosDef m) {lam : ℝ} (hlam : 0 ≤ lam) (hK : ∀ (x : Vec d), Matrix.mulVec K x ⬝ᵥ m⁻¹.mulVec (Matrix.mulVec K x) ≤ lam * x ⬝ᵥ Matrix.mulVec m x) (x : Vec d) : (Matrix.transpose K).mulVec x ⬝ᵥ m⁻¹.mulVec ((Matrix.transpose K).mulVec x) ≤ lam * x ⬝ᵥ Matrix.mulVec m x

The transposed matrix obeys the same normalized bound. If |m^{-1/2}Kx|² ≤ λ|m^{1/2}x|² for every x, the same holds for Kᵗ. The proof is Cauchy–Schwarz in the m metric at the vector m^{-1}Kᵗx.

theorem HCPolySupport.HighContrast.Quenched.quad_responseSkew_le {d : ℕ} {m K : Mat d} (hm : Matrix.PosDef m) {lam : ℝ} (hlam : 0 ≤ lam) (hK : ∀ (x : Vec d), Matrix.mulVec K x ⬝ᵥ m⁻¹.mulVec (Matrix.mulVec K x) ≤ lam * x ⬝ᵥ Matrix.mulVec m x) (x : Vec d) : Matrix.mulVec (Response.responseSkew K) x ⬝ᵥ m⁻¹.mulVec (Matrix.mulVec (Response.responseSkew K) x) ≤ lam * x ⬝ᵥ Matrix.mulVec m x

The antisymmetric part obeys the same normalized bound.

The two-sided comparison of the terminal mean

theorem HCPolySupport.HighContrast.Quenched.schur_skew_quad_le_of_sandwich {d : ℕ} {m : Mat d} {A : BlockMat d} {S SStar K : Mat d} (hS : Matrix.PosDef S) (hform : toFullBlockMat A = schurBlock S SStar K) {C kap : ℝ} (hkap : 0 ≤ kap) (hup : BlockMatLoewnerLE A (blockScale C (Book.Ch02.blockDiag m m⁻¹))) (hlow : BlockMatLoewnerLE (Book.Ch02.blockDiag m m⁻¹) (blockScale kap A)) (x : Vec d) : Matrix.mulVec K x ⬝ᵥ m⁻¹.mulVec (Matrix.mulVec K x) ≤ kap * C * x ⬝ᵥ Matrix.mulVec m x

The normalized Schur coordinate of a two-sidedly comparable block. If the block A with Schur data (S, S_*, K) satisfies A ≤ C M_0 and M_0 ≤ κ A for the split metric M_0 = diag(m,m^{-1}), then |m^{-1/2}Kx|² ≤ κ C |m^{1/2}x|².

theorem HCPolySupport.HighContrast.Quenched.responseSkew_quad_le_of_sandwich {d : ℕ} {m : Mat d} (hm : Matrix.PosDef m) {A : BlockMat d} {S SStar K : Mat d} (hS : Matrix.PosDef S) (hform : toFullBlockMat A = schurBlock S SStar K) {C kap : ℝ} (hC : 0 ≤ C) (hkap : 0 ≤ kap) (hup : BlockMatLoewnerLE A (blockScale C (Book.Ch02.blockDiag m m⁻¹))) (hlow : BlockMatLoewnerLE (Book.Ch02.blockDiag m m⁻¹) (blockScale kap A)) (x : Vec d) : vecDot (matVecMul (Response.responseSkew K) x) (matVecMul m⁻¹ (matVecMul (Response.responseSkew K) x)) ≤ √(kap * C) ^ 2 * vecDot x (matVecMul m x)

The response skew of a two-sidedly comparable block is normalized-small. This is the τ-input of blockSize_skewBlockCongr_reference_le at the recentered reference, where the canonical shear has been removed.