High-contrast homogenization: Provider.Quenched.Prop42Tilt.AdaptedHatIntrinsic #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Intrinsic contrast from the hatted trace carrier #
For a positive doubled block above its sharp, the intrinsic contrast is bounded by a quadratic polynomial in the trace gap
u = tr (σ σ₍⁻¹) - d.
The quadratic term is necessary at unrestricted contrast. The proof uses the sharp ordering after a fixed Schur shear and therefore introduces no smallness assumption.
theorem
HCPolySupport.HighContrast.Quenched.blockContrast_sub_one_le_traceGap_polynomial
{d : ℕ}
[NeZero d]
{F : BlockMat d}
(hsymm : IsSymmetricBlockMat F)
(hpos : Book.Ch02.BlockPosDef F)
(hsharp : BlockMatLoewnerLE (blockSharp F) F)
:
blockContrast F - 1 ≤ 5 / 4 * ((schurSigma F * F.lowerRight).trace - ↑d) + 1 / 4 * ((schurSigma F * F.lowerRight).trace - ↑d) ^ 2
A sharp-ordered positive block has intrinsic contrast controlled by its unnormalized hatted trace gap.
theorem
HCPolySupport.HighContrast.Quenched.adaptedContrast_sub_one_le_hatted_polynomial
{d : ℕ}
[NeZero d]
{P : MeasureTheory.Measure (CoeffSpace d)}
[MeasureTheory.IsProbabilityMeasure P]
{l r : ℤ}
{q : Mat d}
(hq : IsRoundedGrid l q)
(hfin : HasFiniteAdaptedMean P q r)
:
blockContrast (adaptedMean P q r) - 1 ≤ 5 / 4 * ↑d * (adaptedHattedContrast P q r - 1) + 1 / 4 * (↑d * (adaptedHattedContrast P q r - 1)) ^ 2
The generic trace-gap polynomial specialized to the adapted hatted contrast.
theorem
HCPolySupport.HighContrast.Quenched.one_le_adaptedHattedContrast_of_rounded
{d : ℕ}
[NeZero d]
{P : MeasureTheory.Measure (CoeffSpace d)}
[MeasureTheory.IsProbabilityMeasure P]
{l r : ℤ}
{q : Mat d}
(hq : IsRoundedGrid l q)
(hfin : HasFiniteAdaptedMean P q r)
:
The canonical adapted hatted carrier is at least one on a finite rounded adapted mean.