High-contrast homogenization: Provider.Window.BadScaleBound

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

theorem HCPolySupport.HighContrast.Window.measureReal_badScaleEvent_le_geometric {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 m : ℤ} (hQ : 1 ≤ Q) (hw : IsCoupledWindow d Q K jStar M) (hm : M ≤ m) : P.real {a : CoeffSpace d | badScaleEvent g E (M - jStar) m a} ≤ 3 ^ (-(m - (M - jStar))) * (Ψ ((growthBar K ^ (4 * (d + 1)))⁻¹ * 3 ^ (m - (M - jStar))))⁻¹

Coupling absorbs the number of aligned tiles and leaves one geometric factor at each generation.