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

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

Scalarization of the adapted-to-Euclidean tilt comparison

The one-sided block adapter is first absorbed into a multiplicative comparison with the adapted mean. Intrinsic contrast has degree two under a common scalar dilation, so this comparison combines with the hatted-trace polynomial without any additional smallness premise.

theorem HCPolySupport.HighContrast.Quenched.blockContrast_blockScale_le {d : ℕ} {B : BlockMat d} (hBsymm : IsSymmetricBlockMat B) (hBpos : Book.Ch02.BlockPosDef B) {c : ℝ} (hc : 0 < c) : blockContrast (blockScale c B) ≤ c ^ 2 * blockContrast B

Intrinsic contrast grows by at most the square of a positive scalar under scalar dilation of a positive block.

theorem HCPolySupport.HighContrast.Quenched.blockContrast_sub_one_le_adaptedHatted_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)) : have eta := c * blockSize E (adaptedMean P q r); have x := ↑d * (adaptedHattedContrast P q r - 1); blockContrast A - 1 ≤ (1 + eta) ^ 2 * (1 + 5 / 4 * x + 1 / 4 * x ^ 2) - 1

A one-sided adapter error gives a corrected scalar contrast comparison. The error size is measured natively by blockSize E B; no tolerance or smallness hypothesis is added.