High-contrast homogenization: Provider.Quenched.SmallContrastGoodQuads

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

Good quadratic control for ordered Schur data

The change of the Schur coupling between two ordered positive blocks is controlled by the product of their two normalized diagonal gaps. Together with the hatted trace drop, this gives a dimension-sharp linear bound for all three normalized Schur gaps.

theorem HCPolySupport.HighContrast.Quenched.schurSkew_diff_quad_le_of_lowerRight_le {d : ℕ} {C F : BlockMat d} (hCsymm : IsSymmetricBlockMat C) (hCpos : Book.Ch02.BlockPosDef C) (hFsymm : IsSymmetricBlockMat F) (hFpos : Book.Ch02.BlockPosDef F) (hCF : BlockMatLoewnerLE C F) {a : ℝ} (ha : 0 < a) (hscale : F.lowerRight ≤ (1 + a) • C.lowerRight) : Matrix.conjTranspose (schurSkew F - schurSkew C) * C.lowerRight * (schurSkew F - schurSkew C) ≤ a • (schurSigma F - schurSigma C)

If the lower-right fine block is at most 1 + a times the coarse one, then the coarse-normalized square of the Schur-coupling change is at most a times the upper Schur gap.

theorem HCPolySupport.HighContrast.Quenched.schurSkew_diff_quad_le_lowerRight_norm_gap {d : ℕ} {C F : BlockMat d} (hCsymm : IsSymmetricBlockMat C) (hCpos : Book.Ch02.BlockPosDef C) (hFsymm : IsSymmetricBlockMat F) (hFpos : Book.Ch02.BlockPosDef F) (hCF : BlockMatLoewnerLE C F) : Matrix.conjTranspose (schurSkew F - schurSkew C) * C.lowerRight * (schurSkew F - schurSkew C) ≤ ‖matSqrt C.lowerRight⁻¹ * F.lowerRight * matSqrt C.lowerRight⁻¹ - 1‖ • (schurSigma F - schurSigma C)

The optimized shear estimate, including the zero-gap endpoint. Its coefficient is exactly the lower-right normalized spectral gap.

theorem HCPolySupport.HighContrast.Quenched.normalized_schurSkew_diff_le_hattedContrast_drop {d : ℕ} [NeZero d] {C F : BlockMat d} (hCsymm : IsSymmetricBlockMat C) (hCpos : Book.Ch02.BlockPosDef C) (hFsymm : IsSymmetricBlockMat F) (hFpos : Book.Ch02.BlockPosDef F) (hCF : BlockMatLoewnerLE C F) (hCsharp : BlockMatLoewnerLE (blockSharp C) C) : ‖matSqrt C.lowerRight * (schurSkew F - schurSkew C) * matSqrt (schurSigma C)⁻¹‖ ≤ ↑d * (hattedContrast F - hattedContrast C)

The normalized change of the Schur coupling is bounded by the hatted carrier drop. Together with normalized_schur_norm_gaps_le_hattedContrast_drop this is the full good-quadratics estimate.

theorem HCPolySupport.HighContrast.Quenched.normalized_schur_good_quads_le_hattedContrast_drop {d : ℕ} [NeZero d] {C F : BlockMat d} (hCsymm : IsSymmetricBlockMat C) (hCpos : Book.Ch02.BlockPosDef C) (hFsymm : IsSymmetricBlockMat F) (hFpos : Book.Ch02.BlockPosDef F) (hCF : BlockMatLoewnerLE C F) (hCsharp : BlockMatLoewnerLE (blockSharp C) C) : max (‖matSqrt (schurSigma C)⁻¹ * schurSigma F * matSqrt (schurSigma C)⁻¹ - 1‖ + ‖matSqrt C.lowerRight⁻¹ * F.lowerRight * matSqrt C.lowerRight⁻¹ - 1‖) ‖matSqrt C.lowerRight * (schurSkew F - schurSkew C) * matSqrt (schurSigma C)⁻¹‖ ≤ ↑d * (hattedContrast F - hattedContrast C)

The three normalized Schur gaps satisfy the source good-quadratics bound: the sum of the two diagonal gaps and the coupling gap are each charged to the same hatted carrier drop.

theorem HCPolySupport.HighContrast.Quenched.adaptedMean_normalized_schur_good_quads_le_hattedContrast_drop {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (hP : IsStationaryLaw P) {l : ℤ} {q : Mat d} (hq : IsRoundedGrid l q) {j p : ℤ} (hlj : l ≤ j) (hjp : j ≤ p) (hintj : HasFiniteAdaptedMean P q j) (hintp : HasFiniteAdaptedMean P q p) : max (‖matSqrt (schurSigma (adaptedMean P q p))⁻¹ * schurSigma (adaptedMean P q j) * matSqrt (schurSigma (adaptedMean P q p))⁻¹ - 1‖ + ‖matSqrt (adaptedMean P q p).lowerRight⁻¹ * (adaptedMean P q j).lowerRight * matSqrt (adaptedMean P q p).lowerRight⁻¹ - 1‖) ‖matSqrt (adaptedMean P q p).lowerRight * (schurSkew (adaptedMean P q j) - schurSkew (adaptedMean P q p)) * matSqrt (schurSigma (adaptedMean P q p))⁻¹‖ ≤ ↑d * (adaptedHattedContrast P q j - adaptedHattedContrast P q p)

Good quadratics on one rounded adapted grid, with the later scale as the coarse normalization.