High-contrast homogenization: Provider.Quenched.SmallContrastRecenteredSharp

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

The recentered annealed block: Schur data and sharp order

Recentering the coefficient field by the constant skew g replaces the annealed block by its shear congruence, whose Schur coordinate drops by g while the two diagonal Schur data are unchanged. The sharp order for the recentered block follows from the pathwise toolkit at the recentered samples and matrix Jensen — not from a congruence of the original sharp order, which is false in general.

theorem HCPolySupport.HighContrast.Quenched.toFullBlockMat_skewBlockCongr_of_schurBlock {d : ℕ} {A : BlockMat d} {S SStar K : Mat d} (g : Mat d) (hE : toFullBlockMat A = schurBlock S SStar K) : toFullBlockMat (Response.skewBlockCongr g A) = schurBlock S SStar (K - g)

The Schur representation of a shear congruence: the skew coordinate drops by the shear while both diagonal coordinates persist.

theorem HCPolySupport.HighContrast.Quenched.blockSharp_skewBlockCongr_annealedBlock_le {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (U : Book.Ch02.Domain d) (hint : HasIntegrableCoarseBlock P U.carrier) (g : Mat d) (hg : IsSkewMat g) : BlockMatLoewnerLE (blockSharp (Response.skewBlockCongr g (annealedBlock P U.carrier))) (Response.skewBlockCongr g (annealedBlock P U.carrier))

The sharp order for the recentered annealed block. The pathwise positivity and pathwise sharp order hold at every sample, in particular at the recentered samples; matrix Jensen then gives the annealed sharp order for the recentered mean. Both toolkit facts are theorems of the coarse-block positivity module, so the only hypothesis on the law is integrability.