High-contrast homogenization: Provider.Quenched.Prop42Tilt.CorrectedTiltAdapter

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

The native corrected tilt adapter

This is the reverse half of the adapted-to-Euclidean block adapter, scalarized through the adapted hatted contrast. Its scale and error coefficient are exactly those supplied by the block theorem.

theorem HCPolySupport.HighContrast.Quenched.tilt_scalar_polynomial_le {eta x : ℝ} (heta0 : 0 ≤ eta) (heta1 : eta ≤ 1) (hx0 : 0 ≤ x) (hx1 : x ≤ 1) : (1 + eta) ^ 2 * (1 + 5 / 4 * x + 1 / 4 * x ^ 2) - 1 ≤ 9 / 2 * (eta + x)

On the unit box for the absorbed adapter size and hatted trace gap, the quadratic scalarization is bounded by the sharp convenient factor 9/2.

theorem HCPolySupport.HighContrast.Quenched.blockContrast_sub_one_le_tilt_sum_of_adapter {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {A E : BlockMat d} {l r : ℤ} {q : Mat d} (hAsymm : IsSymmetricBlockMat A) (hApos : Book.Ch02.BlockPosDef A) (hEsymm : IsSymmetricBlockMat E) (hEpos : Book.Ch02.BlockPosDef E) (hq : IsRoundedGrid l q) (hfin : HasFiniteAdaptedMean P q r) {c : ℝ} (hc : 0 ≤ c) (hsub : BlockMatLoewnerLE (blockSub A (adaptedMean P q r)) (blockScale c E)) (heta1 : c * blockSize E (adaptedMean P q r) ≤ 1) (hx1 : ↑d * (adaptedHattedContrast P q r - 1) ≤ 1) : blockContrast A - 1 ≤ 9 / 2 * (↑d * (adaptedHattedContrast P q r - 1)) + 9 / 2 * (c * blockSize E (adaptedMean P q r))

The form consumed by the corrected scalar transfer. Once the native adapter size and the dimension-rescaled hatted gap are at most one, the Euclidean intrinsic contrast is the sum of a hatted term and an adapter term, both with coefficient 9/2.