High-contrast homogenization: Provider.Window.SuccessorTail

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

theorem HCPolySupport.HighContrast.Window.measureReal_successorScale_tail {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (hstat : IsStationaryLaw P) {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K Q : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) {jStar M : ℤ} (hQ : 1 ≤ Q) (hw : IsCoupledWindow d Q K jStar M) {t : ℝ} (ht : 1 ≤ t) : P.real {a : CoeffSpace d | ENNReal.ofReal (max (3 ^ M) (t * growthBar K ^ (4 * (d + 1)) * 3 ^ (M - jStar + 1))) < successorScale g E (M - jStar) a} ≤ (Ψ t)⁻¹

The strict successor has the continuous source-gauge tail with the printed maximum at the terminal generation.

theorem HCPolySupport.HighContrast.Window.ae_successorScale_ne_top {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (hstat : IsStationaryLaw P) {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K Q : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) {jStar M : ℤ} (hQ : 1 ≤ Q) (hw : IsCoupledWindow d Q K jStar M) : ∀ᵐ (a : CoeffSpace d) ∂P, successorScale g E (M - jStar) a ≠ ⊤

The strict successor is finite almost surely.