OAI/Analysis/FiniteFactor/CrossedProduct/FutureBoundary.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.sourceBiasedCoordinate_measure line 11
2. def OAI.FiniteFactor.sourceFutureBad line 21
3. def OAI.FiniteFactor.sourceFutureBoundaryEvent line 25
4. theorem OAI.FiniteFactor.sourceFutureBad_measurable line 28
5. theorem OAI.FiniteFactor.sourceFutureBoundaryEvent_measurable line 34
6. theorem OAI.FiniteFactor.sourceFutureBad_bound line 38

   Source documentation

   The actual one-coordinate contribution to the future union loss.

   theorem sourceFutureBad_bound (j n : ℕ) (i : Fin (sourceBlockSize (j+1+n))) :
       (sourceBiasedLaw j) (sourceFutureBad j n i) ≤
         ENNReal.ofReal (20*sourceExclusionWidth j ⟨j+1+n,i⟩) := by
   …

   Mentions: OAI.FiniteFactor.sourceBlockSize, OAI.FiniteFactor.sourceBiasedLaw, OAI.FiniteFactor.sourceFutureBad, OAI.FiniteFactor.sourceExclusionWidth

7. theorem OAI.FiniteFactor.sourceFutureBoundary_no_bad line 56