EventMassUpper.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.sourceProjectionEvent_mass_upper line 12
Source documentation
An invariant projection in the original algebra forces the actual source event to have mass at most 1/(j+1) whenever the fixed-angle phase condition holds. Every coefficient, convolution and expectation input is discharged.
```
theorem sourceProjectionEvent_mass_upper (θ : SourceCoordinate → ℝ) (hθ : SourceAngles θ)
    (hs : SourceOrderedTorusSampling θ)
    {p : SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate}
    (hp : p ∈ sourceAlgebra θ) (hproj : IsStarProjection p)
    (hinv : (1-p)*sourceOperator θ sourceLogWeight hθ.nonneg sourceLogWeight_nonneg*p = 0)
    (j : ℕ) (hphase : SourceSecondPhasesFrom θ j) :
    (sourceBiasedLaw j).real (sourceProjectionEvent p j) ≤ 1/((j : ℝ)+1) := by
…
```
Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceAngles, OAI.FiniteFactor.SourceOrderedTorusSampling, OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.sourceAlgebra, OAI.FiniteFactor.sourceOperator, OAI.FiniteFactor.sourceLogWeight, OAI.FiniteFactor.sourceLogWeight_nonneg, OAI.FiniteFactor.SourceSecondPhasesFrom, OAI.FiniteFactor.sourceBiasedLaw, OAI.FiniteFactor.sourceProjectionEvent