High-contrast homogenization: Provider.Quenched.SmallContrastMeanDilation

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

Fine-to-coarse dilation from the hatted contrast drop

The positive adapted-mean increment is measured in the coarse Schur geometry. Its two diagonal trace gaps are linear in the hatted drop. The coupling term is quadratic, by the good-quadratics estimate, and is absorbed in the perturbative range. This yields the full-block dilation used by the calibrated profile defects.

theorem HCPolySupport.HighContrast.Quenched.adaptedMean_le_hattedContrast_dilation {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (hstat : IsStationaryLaw P) {l : ℤ} {q : Mat d} (hgrid : IsRoundedGrid l q) {j p : ℤ} (hlj : l ≤ j) (hjp : j ≤ p) (hfinj : HasFiniteAdaptedMean P q j) (hfinp : HasFiniteAdaptedMean P q p) (hsmall : ↑d * (adaptedHattedContrast P q j - adaptedHattedContrast P q p) ≤ 1) : toFullBlockMat (adaptedMean P q j) ≤ (1 + 4 * ↑d * (adaptedHattedContrast P q j - adaptedHattedContrast P q p)) • toFullBlockMat (adaptedMean P q p)

In the perturbative range, the hatted-carrier drop controls the complete fine adapted mean in the geometry of the coarse adapted mean.