MaskedError.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.sourceOmitted_masked_error line 14
Source documentation
Both source expected-error estimates for the full infinite coefficient sum. b=false,r=0,s=n gives the first orientation; b=true,r=n,s=0 gives the second, after commuting the scalar product.
```
theorem sourceOmitted_masked_error (θ : SourceCoordinate → ℝ) (hθ : SourceAngles θ)
    {p : SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate}
    (hp : p ∈ sourceAlgebra θ) (hproj : IsStarProjection p)
    (j : ℕ) (hphase : SourceSecondPhasesFrom θ j) (n r s : ℤ) (b : Bool) :
    let error := fun ω => ∑' k : ℤ, (sourceOmittedBadEvent θ hθ j hphase n k b).indicator
…
```
Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceAngles, OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.sourceAlgebra, OAI.FiniteFactor.SourceSecondPhasesFrom, OAI.FiniteFactor.sourceOmittedBadEvent