OAI/Analysis/FiniteFactor/CrossedProduct/ProjectionErrors.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.indicator_swap line 15

   Source documentation

   Exchange the coefficient and sample viewpoints of the same mask.

   theorem indicator_swap {ι Ω : Type*} (H : ι → Set Ω) (f : ι → Ω → ℝ) (i : ι) (ω : Ω) :
       {k | ω ∈ H k}.indicator (fun k => f k ω) i = (H i).indicator (f i) ω := by
   …

2. def OAI.FiniteFactor.sourceTruncatedCoefficient line 22
3. def OAI.FiniteFactor.sourceOmittedError line 29
4. theorem OAI.FiniteFactor.sourceOmittedError_nonneg line 36
5. theorem OAI.FiniteFactor.sourceOmittedError_estimate line 43

   Source documentation

   Both actual infinite error sums are integrable and have the source bound.

   theorem sourceOmittedError_estimate (θ : SourceCoordinate → ℝ) (hθ : SourceAngles θ)
       {p : SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate}
       (hp : p ∈ sourceAlgebra θ) (hproj : IsStarProjection p)
       (j : ℕ) (hphase : SourceSecondPhasesFrom θ j) (n : ℤ) (b : Bool) :
       Integrable (sourceOmittedError θ hθ p j hphase n b) (sourceBiasedLaw j) ∧
         (∫ ω, sourceOmittedError θ hθ p j hphase n b ω ∂sourceBiasedLaw j) ≤ Real.exp (-(sourceStage j).L/800) := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceAngles, OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.sourceAlgebra, OAI.FiniteFactor.SourceSecondPhasesFrom, OAI.FiniteFactor.sourceOmittedError, OAI.FiniteFactor.sourceBiasedLaw, OAI.FiniteFactor.sourceStage

6. theorem OAI.FiniteFactor.sourceProjectionEvent_error_pointwise line 56