EventPositive.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.sourceProjectionEvent_eventually_positive line 14
Source documentation
The actual source E_j has an eventual fixed positive lower bound for any nontrivial invariant projection of the original algebra. The threshold may depend on p; the positive lower bound does not.
```
theorem sourceProjectionEvent_eventually_positive
    (θ : SourceCoordinate → ℝ) (hθ : SourceAngles θ) (hr : SourceRationalIndependent θ)
    {p : SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate}
    (hp : p ∈ sourceAlgebra θ) (hproj : IsStarProjection p) (hp0 : p ≠ 0) (hp1 : p ≠ 1)
    (hinv : (1-p)*sourceOperator θ sourceLogWeight hθ.nonneg sourceLogWeight_nonneg*p = 0) :
    ∀ᶠ j : ℕ in atTop, Real.exp (-82)/2 ≤ (sourceBiasedLaw j).real (sourceProjectionEvent p j) := by
…
```
Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceAngles, OAI.FiniteFactor.SourceRationalIndependent, OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.sourceAlgebra, OAI.FiniteFactor.sourceOperator, OAI.FiniteFactor.sourceLogWeight, OAI.FiniteFactor.sourceLogWeight_nonneg, OAI.FiniteFactor.sourceBiasedLaw, OAI.FiniteFactor.sourceProjectionEvent