High-contrast homogenization: Provider.Quenched.SmallContrastSkewInvariants

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

Scalar invariance of the contrasts under a constant-skew recentering

The observation of Section 2.5 of HC, equation (2.65), is that subtracting a constant skew g from the coefficient field leaves σ and σ_* untouched and replaces k by k - g. Both contrasts of the paper are functions of the Schur data that are blind to the skew coordinate — the hatted contrast does not mention it, and the intrinsic contrast minimizes over it — so both are invariant.

This file records that invariance at the level of doubled blocks, which is the algebraic half of the law-side API for that recentering: once annealedBlock (P.map (·.subSkew g hg)) U = skewBlockCongr g (annealedBlock P U) is available, annealedContrast and adaptedHattedContrast are literally unchanged by the recentering.

Reading the Schur data off a Schur form

theorem HCPolySupport.HighContrast.Quenched.schurData_of_schurBlock {d : ℕ} {H : BlockMat d} {S SStar K : Mat d} (hStar : Matrix.PosDef SStar) (hH : toFullBlockMat H = schurBlock S SStar K) : H.lowerRight = SStar⁻¹ ∧ schurSigmaStar H = SStar ∧ schurSkew H = K ∧ schurSigma H = S

The Schur data of a block in Schur form is the data of the form.

The hatted contrast is skew-blind

The intrinsic contrast is skew-blind

def HCPolySupport.HighContrast.Quenched.contrastSet {d : ℕ} (S SStar K : Mat d) : Set ℝ

The defining set of the intrinsic contrast, written in Schur data.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.Quenched.blockContrast_skewBlockCongr {d : ℕ} {H : BlockMat d} {S SStar K : Mat d} (hStar : Matrix.PosDef SStar) (hH : toFullBlockMat H = schurBlock S SStar K) {g : Mat d} (hg : IsSkewMat g) : blockContrast (Response.skewBlockCongr g H) = blockContrast H

The intrinsic contrast is invariant under a constant-skew recentering. The minimization over the skew coordinate absorbs the shift.