OAI/Analysis/FiniteFactor/CrossedProduct/OmittedRatio.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.sourceOmitted_ratio_bound line 14

   Source documentation

   The source two-ratio inequality and deterministic omitted-index choice turn tagged and phase attenuation into the pointwise error majorant.

   theorem sourceOmitted_ratio_bound (θ : SourceCoordinate → ℝ) (hθ : SourceAngles θ)
       (j : ℕ) (hphase : SourceSecondPhasesFrom θ j) (n v : ℤ) (hn : 0 ≤ n)
       (hv : ((sourceStageState j).K : ℤ) < |v| ∨ ((sourceStageState j).K : ℤ) < |n+v|) :
       ∀ᵐ ω ∂sourceBiasedLaw j, ω ∈ sourceTagEndpointEvent j →
         sourceCocycle θ sourceLogWeight (n+v) (sourceBiasedEndpoint (fun _ => true) ω) /
           sourceCocycle θ sourceLogWeight v (sourceBiasedEndpoint (fun _ => false) ω) ≤
             Real.exp (-(sourceStage j).L) +
               (sourceOmittedBadEvent θ hθ j hphase n v false).indicator (fun _ => (1 : ℝ)) ω +
               (sourceOmittedBadEvent θ hθ j hphase n v true).indicator (fun _ => (1 : ℝ)) ω := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceAngles, OAI.FiniteFactor.SourceSecondPhasesFrom, OAI.FiniteFactor.sourceStageState, OAI.FiniteFactor.sourceBiasedLaw, OAI.FiniteFactor.sourceTagEndpointEvent, OAI.FiniteFactor.sourceCocycle, OAI.FiniteFactor.sourceLogWeight, OAI.FiniteFactor.sourceBiasedEndpoint, OAI.FiniteFactor.sourceStage, OAI.FiniteFactor.sourceOmittedBadEvent