OAI/Analysis/MarkovType/FiniteDyadicProbability.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MarkovSuperreflexivity.DyadicWord line 16
  2. def OAI.MarkovSuperreflexivity.fairBitLaw line 18
  3. def OAI.MarkovSuperreflexivity.dyadicLaw line 23
  4. theorem OAI.MarkovSuperreflexivity.dyadicLaw_mass line 25
  5. theorem OAI.MarkovSuperreflexivity.fairBitLaw_prob_eq line 29
  6. def OAI.MarkovSuperreflexivity.dyadicFiltration line 33
  7. def OAI.MarkovSuperreflexivity.dyadicPrefix line 44
  8. theorem OAI.MarkovSuperreflexivity.dyadicPrefix_eq_of_rel line 47
  9. theorem OAI.MarkovSuperreflexivity.dyadic_rel_of_prefix_eq line 53
  10. theorem OAI.MarkovSuperreflexivity.dyadic_prod_initial line 59
  11. theorem OAI.MarkovSuperreflexivity.dyadicLaw_prob_prefix line 81
  12. theorem OAI.MarkovSuperreflexivity.FiniteLaw.expect_eq_sum_fiber line 112
  13. theorem OAI.MarkovSuperreflexivity.dyadicLaw_expect_prefix line 124
  14. def OAI.MarkovSuperreflexivity.dyadicFlip line 130
  15. theorem OAI.MarkovSuperreflexivity.dyadicFlip_at line 133
  16. theorem OAI.MarkovSuperreflexivity.dyadicFlip_of_ne line 136
  17. theorem OAI.MarkovSuperreflexivity.dyadicFlip_involutive line 139
  18. def OAI.MarkovSuperreflexivity.dyadicFlipEquiv line 147
  19. theorem OAI.MarkovSuperreflexivity.dyadicFlip_rel line 153
  20. theorem OAI.MarkovSuperreflexivity.dyadicFlip_prefix line 161