High-contrast homogenization: Provider.Quenched.SmallContrastCorrectedEndpointCore

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

theorem endpoint_hcore_body_corrected_core (d : ℕ) (hd : 2 ≤ d) (g : ℝ) : g ∈ Set.Ico 0 1 → ∃ (cSc : ℝ), 0 < cSc ∧ ∃ (alpha : ℝ) (Cdelay : ℝ), 0 < alpha ∧ 0 ≤ Cdelay ∧ ∀ (cStar gBase : ℝ) (Pbase : MeasureTheory.Measure (HCPolySupport.HighContrast.CoeffSpace d)) (Ebase : HCPolySupport.BlockMat d) (Ψbase : ℝ → ℝ) (Kbase : ℝ) (Sbase : HCPolySupport.HighContrast.CoeffSpace d → ℝ), cStar ∈ Set.Ioc 0 cSc → gBase = (1 + g) / 2 → MeasureTheory.IsProbabilityMeasure Pbase → HCPoly.Frozen.IsStationaryLaw Pbase → HCPoly.Frozen.IsUnitRangeLaw Pbase → HCPoly.Frozen.CoarseEllipticityDagger Pbase gBase Ebase Ψbase Kbase Sbase → HCPolySupport.HighContrast.annealedContrast Pbase 0 - 1 ≤ cStar → HCPolySupport.HighContrast.blockContrast Ebase ≤ 1 + cSc → ∃ (m0 : ℕ), 3 ^ m0 ≤ (2 + HCPolySupport.HighContrast.aspectRatio Ebase * Kbase) ^ Cdelay ∧ ∀ (j : ℕ), HCPolySupport.HighContrast.annealedContrast Pbase ↑(m0 + j) - 1 ≤ 3 ^ (-alpha * ↑j)