EventExpectation.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.sourceProjectionEvent_coefficient_expectation line 12
Source documentation
The source per-coefficient expectation upper bound, with all convolution, ratio and masked-error inputs discharged for the original invariant p.
```
theorem sourceProjectionEvent_coefficient_expectation (θ : 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) (n : ℕ) :
    (∫ ω in sourceProjectionEvent p j, ‖sourceTruncatedCoefficient θ p j n ω‖ ∂sourceBiasedLaw j) ≤
      Real.exp (-(sourceStage j).L)+2*Real.exp (-(sourceStage j).L/800) := 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.sourceProjectionEvent, OAI.FiniteFactor.sourceTruncatedCoefficient, OAI.FiniteFactor.sourceBiasedLaw, OAI.FiniteFactor.sourceStage