ProjectionEvent.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.FiniteFactor.sourceDiagonalEvent line 12
theorem OAI.FiniteFactor.sourceDiagonalEvent_measurable line 17
def OAI.FiniteFactor.sourceProjectionEvent line 28
Source documentation
The actual three conditions defining E_j in the source, with j+1 indexing.
```
def sourceProjectionEvent
    (p : SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate) (j : ℕ) : Set SourceBiasedSample :=
…
```
Mentions: OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceBiasedSample
theorem OAI.FiniteFactor.sourceProjectionEvent_measurable line 32

theorem OAI.FiniteFactor.sourceProjection_zero_coefficients line 39

Source documentation

The zero coefficient bounds use the actual diagonal and F_0=1.

theorem sourceProjection_zero_coefficients (θ : SourceCoordinate → ℝ)
    (p : SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate) (j : ℕ) :
    ∀ᵐ ω ∂sourceBiasedLaw j, ω ∈ sourceDiagonalEvent p j →
      1/((j : ℝ)+1) ≤ ‖sourceProjectionLeftCoefficient θ p (sourceBiasedEndpoint (fun _ => false) ω) 0‖ ∧
      1/((j : ℝ)+1) ≤ ‖sourceProjectionRightCoefficient θ p (sourceBiasedEndpoint (fun _ => true) ω) 0‖ := by
…

Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.sourceBiasedLaw, OAI.FiniteFactor.sourceDiagonalEvent, OAI.FiniteFactor.sourceProjectionLeftCoefficient, OAI.FiniteFactor.sourceBiasedEndpoint, OAI.FiniteFactor.sourceProjectionRightCoefficient

theorem OAI.FiniteFactor.sourceProjectionEvent_polynomial_lower line 66
Source documentation
The actual source-stage polynomial lower bound holds on the exact E_j. This theorem does not assert that E_j has positive probability.
```
theorem sourceProjectionEvent_polynomial_lower (θ : SourceCoordinate → ℝ) (hθ : SourceAngles θ)
    {p : SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate}
    (hp : p ∈ sourceAlgebra θ) (hproj : IsStarProjection p) (j : ℕ) :
    ∀ᵐ ω ∂sourceBiasedLaw j, ω ∈ sourceProjectionEvent p j →
      (sourceStage j).ε ≤ coefficientMass (sourceStageState j).K
        (sourceProjectionLeftCoefficient θ p (sourceBiasedEndpoint (fun _ => false) ω))
        (sourceProjectionRightCoefficient θ p (sourceBiasedEndpoint (fun _ => true) ω)) := by
…
```
Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceAngles, OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.sourceAlgebra, OAI.FiniteFactor.sourceBiasedLaw, OAI.FiniteFactor.sourceProjectionEvent, OAI.FiniteFactor.sourceStage, OAI.FiniteFactor.coefficientMass, OAI.FiniteFactor.sourceStageState, OAI.FiniteFactor.sourceProjectionLeftCoefficient, OAI.FiniteFactor.sourceBiasedEndpoint, OAI.FiniteFactor.sourceProjectionRightCoefficient