High-contrast homogenization: Provider.Quenched.SmallContrastProfileDefectCap

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

Calibrated profile defects from the hatted mean dilation

The canonical Schur recentering uses the unshifted metric loads in the profile defects. The opposite shifts occur only when constant-skew covariance rewrites the resulting terminal calls back to the original coefficient field.

This file isolates the last algebraic input needed for the two defect caps. If the fine adapted mean is bounded by the coarse adapted mean with the dilation predicted by the hatted-carrier drop, response-load calibration turns that matrix comparison into dimension-only bounds for both profile defects.

theorem HCPolySupport.HighContrast.Quenched.calibratedProfileDefects_le_of_hattedMeanDilation {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (hstat : IsStationaryLaw P) {l : ℤ} {qGrid : Mat d} (hgrid : IsRoundedGrid l qGrid) {s t : ℤ} (hls : l ≤ s) (hst : s ≤ t) (hfins : HasFiniteAdaptedMean P qGrid s) (hfint : HasFiniteAdaptedMean P qGrid t) {S SStar K : Mat d} (hS : Matrix.PosDef S) (hStar : Matrix.PosDef SStar) (hEtform : toFullBlockMat (adaptedMean P qGrid t) = schurBlock S SStar K) (hsmall : 6 * (blockContrast (adaptedMean P qGrid t) - 1) ≤ 1) (hupper : toFullBlockMat (adaptedMean P qGrid s) ≤ (1 + 4 * ↑d * (adaptedHattedContrast P qGrid s - adaptedHattedContrast P qGrid t)) • toFullBlockMat (adaptedMean P qGrid t)) (e : Vec d) (he : e ⬝ᵥ e = 1) : let h0 := Response.responseSkew K; have p := Response.centeredResponseLoadP S SStar K e; have r := Response.centeredResponseLoadQ S SStar K e; Response.profilePrimalResponseDefect P ⋯ h0 ⋯ s t p r ≤ 16 * ↑d * (adaptedHattedContrast P qGrid s - adaptedHattedContrast P qGrid t) ∧ Response.profileAdjointResponseDefect P ⋯ h0 ⋯ s t p r ≤ 16 * ↑d * (adaptedHattedContrast P qGrid s - adaptedHattedContrast P qGrid t)

The two canonical profile defects are controlled by the hatted-carrier drop once the corresponding fine-to-coarse mean dilation is known. The terminal intrinsic smallness is written in precisely the form needed to bound the calibrated load energy by an absolute constant.