High-contrast homogenization: Provider.Window.SuccessorDiscrete #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
theorem
HCPolySupport.HighContrast.Window.badScaleEvent_tail_summable
{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 n : ℤ}
(hQ : 1 ≤ Q)
(hw : IsCoupledWindow d Q K jStar M)
(hn : M ≤ n)
:
The bad generations above a coupled window have summable probabilities.
theorem
HCPolySupport.HighContrast.Window.tsum_measureReal_badScaleEvent_le
{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 n : ℤ}
(hQ : 1 ≤ Q)
(hw : IsCoupledWindow d Q K jStar M)
(hn : M ≤ n)
:
The total probability of all bad generations above n is controlled by
the gauge at generation n.
theorem
HCPolySupport.HighContrast.Window.measureReal_successorScale_gt_zpow_le
{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 n : ℤ}
(hQ : 1 ≤ Q)
(hw : IsCoupledWindow d Q K jStar M)
(hn : M ≤ n)
:
The strict successor has the discrete gauge tail at every generation above the coupled window.