High-contrast homogenization: Provider.Quenched.SmallContrastRowAtCenters

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

The hatted quadratic load at the calibrated profile centers

The row caps majorize the earlier rows by the hatted reference quadratic load at the profile centers. Here that load is second order in the hatted contrast defect: the centers are the closed Schur pairs of the terminal mean, the reference is comparable to the terminal mean through the carried deterministic comparability, and the mean's own hatted quadratic load at the closed pairs is controlled by the center magnitudes and the smallness pack. The final constant is κ_ref · 36·(1 + d)·ε² in both orientations.

theorem HCPolySupport.HighContrast.Quenched.profileQuadraticLoad_hatted_primal_center_le {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (hint : HasFiniteAdaptedMean P q t) {S SStar K : Mat d} (hS : Matrix.PosDef S) (hStar : Matrix.PosDef SStar) (hform : toFullBlockMat (adaptedMean P q t) = schurBlock S SStar K) {eps : ℝ} (hpos : 0 < eps) (heps1 : eps ≤ 1) (htr : ↑d * (schurHattedContrast S SStar - 1) ≤ eps) {E : BlockMat d} {kap : ℝ} (hkap0 : 0 ≤ kap) (hcomp : ∀ (X : BlockVec d), blockVecDot X (blockMatVecMul E X) ≤ kap * blockVecDot X (blockMatVecMul (adaptedMean P q t) X)) (e : Vec d) (he : e ⬝ᵥ e = 1) : Response.profileQuadraticLoad (Response.profileHattedBlock (Response.responseSkew K) E) (Response.profilePrimalCenter P hq t (fun (a : CoeffSpace d) => a.subSkew (Response.responseSkew K) ⋯) (Response.centeredResponseLoadP S SStar K e) (Response.centeredResponseLoadQ S SStar K e)).1 (Response.profilePrimalCenter P hq t (fun (a : CoeffSpace d) => a.subSkew (Response.responseSkew K) ⋯) (Response.centeredResponseLoadP S SStar K e) (Response.centeredResponseLoadQ S SStar K e)).2 ≤ kap * (36 * (1 + ↑d) * eps ^ 2)

The hatted reference quadratic load at the primal center is at most κ_ref · 36·(1+d)·ε².

theorem HCPolySupport.HighContrast.Quenched.profileQuadraticLoad_hatted_adjoint_center_le {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (hint : HasFiniteAdaptedMean P q t) {S SStar K : Mat d} (hS : Matrix.PosDef S) (hStar : Matrix.PosDef SStar) (hform : toFullBlockMat (adaptedMean P q t) = schurBlock S SStar K) {eps : ℝ} (hpos : 0 < eps) (heps1 : eps ≤ 1) (htr : ↑d * (schurHattedContrast S SStar - 1) ≤ eps) {E : BlockMat d} {kap : ℝ} (hkap0 : 0 ≤ kap) (hcomp : ∀ (X : BlockVec d), blockVecDot X (blockMatVecMul E X) ≤ kap * blockVecDot X (blockMatVecMul (adaptedMean P q t) X)) (e : Vec d) (he : e ⬝ᵥ e = 1) : Response.profileQuadraticLoad (Response.profileHattedAdjointBlock (Response.responseSkew K) E) (Response.profileAdjointCenter P hq t (fun (a : CoeffSpace d) => a.subSkew (Response.responseSkew K) ⋯) (Response.centeredResponseLoadP S SStar K e) (Response.centeredResponseLoadQ S SStar K e)).1 (Response.profileAdjointCenter P hq t (fun (a : CoeffSpace d) => a.subSkew (Response.responseSkew K) ⋯) (Response.centeredResponseLoadP S SStar K e) (Response.centeredResponseLoadQ S SStar K e)).2 ≤ kap * (36 * (1 + ↑d) * eps ^ 2)

The hatted reference quadratic load at the adjoint center is at most κ_ref · 36·(1+d)·ε².