High-contrast homogenization: Provider.Quenched.SmallContrastDefectComposition

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

The calibrated profile defects from the hatted drop alone

Composing the fine-to-coarse mean dilation with the profile-defect cap removes the dilation hypothesis: on one fixed rounded grid, a small hatted-carrier drop and terminal intrinsic smallness bound both canonical calibrated profile defects by 16 d times the drop. This is the mechanical composition of adaptedMean_le_hattedContrast_dilation with calibratedProfileDefects_le_of_hattedMeanDilation at j = s, p = t.

theorem HCPolySupport.HighContrast.Quenched.calibratedProfileDefects_le_of_smallDrop {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) (hdrop : ↑d * (adaptedHattedContrast P qGrid s - adaptedHattedContrast P qGrid t) ≤ 1) (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 drop. On one fixed rounded grid, if the hatted drop from s to t is perturbatively small and the terminal intrinsic contrast is small, then both calibrated profile defects at the Schur representation of the terminal adapted mean are at most 16 d times the hatted drop.