OAI/Analysis/FiniteFactor/CrossedProduct/OmittedBadEvents.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.sourceOmittedBadEvent line 13

   Source documentation

   The source omitted-index masks. Near tagged indices and retained terms have empty masks. Far assignments depend on n,v and fixed angles only.

   def sourceOmittedBadEvent (θ : SourceCoordinate → ℝ) (hθ : SourceAngles θ)
       (j : ℕ) (hphase : SourceSecondPhasesFrom θ j) (n v : ℤ) (b : Bool) :
       Set SourceBiasedSample :=
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceAngles, OAI.FiniteFactor.SourceSecondPhasesFrom, OAI.FiniteFactor.SourceBiasedSample

2. theorem OAI.FiniteFactor.sourceOmittedBadEvent_measurable line 21
3. theorem OAI.FiniteFactor.sourceOmittedBadEvent_condExp line 31

   Source documentation

   All actual omitted masks obey the same conditional bound, in each orientation and simultaneously over every integer shift and coefficient.

   theorem sourceOmittedBadEvent_condExp (θ : SourceCoordinate → ℝ) (hθ : SourceAngles θ)
       (j : ℕ) (hphase : SourceSecondPhasesFrom θ j) :
       ∀ᵐ ω ∂sourceBiasedLaw j, ∀ (n v : ℤ) (b : Bool),
         (sourceBiasedLaw j)[(sourceOmittedBadEvent θ hθ j hphase n v b).indicator (fun _ => (1 : ℝ)) |
           (inferInstance : MeasurableSpace (SourceCoordinate → ℝ)).comap
             (sourceBiasedEndpoint (fun _ => b))] ω ≤ Real.exp (-(sourceStage j).L/400) := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceAngles, OAI.FiniteFactor.SourceSecondPhasesFrom, OAI.FiniteFactor.sourceBiasedLaw, OAI.FiniteFactor.sourceOmittedBadEvent, OAI.FiniteFactor.sourceBiasedEndpoint, OAI.FiniteFactor.sourceStage