High-contrast homogenization: Provider.Quenched.SmallContrastCenteringSmallness

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

The smallness clauses for the centering estimate

The two matrix smallness hypotheses and the two trace bounds consumed by the generic centering estimate, derived from the hatted contrast of the annealed block alone: the normalized Schur excess has trace d·(hat − 1) and is positive semidefinite, so the diagonal gap is ε-small in the Loewner order; the recentered sharp order and the symmetric-skew bound make the symmetric skew coordinate ε/2-small in the same normalized sense.

theorem HCPolySupport.HighContrast.Quenched.trace_gap_eq_trace_centeredResponseX {d : ℕ} {S SStar : Mat d} (hStar : Matrix.PosDef SStar) : ((S - SStar) * SStar⁻¹).trace = Matrix.trace (Response.centeredResponseX S SStar)

The gap trace in normalized form.

theorem HCPolySupport.HighContrast.Quenched.gap_le_smul_of_trace {d : ℕ} {S SStar : Mat d} (hStar : Matrix.PosDef SStar) (horder : SStar ≤ S) {eps : ℝ} (htr : Matrix.trace (Response.centeredResponseX S SStar) ≤ eps) : S - SStar ≤ eps • SStar

The Loewner form of the diagonal gap from its trace.

theorem HCPolySupport.HighContrast.Quenched.centering_smallness_supply {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (U : Book.Ch02.Domain d) (hint : HasIntegrableCoarseBlock P U.carrier) {S SStar K : Mat d} (hS : Matrix.PosDef S) (hStar : Matrix.PosDef SStar) (hE : toFullBlockMat (annealedBlock P U.carrier) = schurBlock S SStar K) {eps : ℝ} (hpos : 0 < eps) (htr : ↑d * (schurHattedContrast S SStar - 1) ≤ eps) : SStar ≤ S ∧ S - SStar ≤ eps • SStar ∧ Response.responseSymmetric K * SStar⁻¹ * Response.responseSymmetric K ≤ (eps ^ 2 / 4) • SStar ∧ ((S - SStar) * SStar⁻¹).trace ≤ eps ∧ (Response.responseSymmetric K * SStar⁻¹ * Response.responseSymmetric K * SStar⁻¹).trace ≤ ↑d * eps ^ 2 / 4

The smallness supply for the centering estimate. From the annealed block's Schur representation and the hatted-contrast bound d·(hat − 1) ≤ ε alone: the diagonal order, the two Loewner smallness clauses, and the two trace bounds, exactly as the generic centering estimate consumes them.