OAI/Analysis/MarkovType/FiniteDyadicMartingale.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MarkovSuperreflexivity.DyadicAtom line 16
  2. def OAI.MarkovSuperreflexivity.dyadicInputWeight line 18
  3. theorem OAI.MarkovSuperreflexivity.dyadicInputWeight_nonneg line 22
  4. def OAI.MarkovSuperreflexivity.dyadicRoot line 28
  5. def OAI.MarkovSuperreflexivity.dyadicCoefficient line 30
  6. def OAI.MarkovSuperreflexivity.dyadicSign line 33
  7. theorem OAI.MarkovSuperreflexivity.dyadicSign_not line 35
  8. def OAI.MarkovSuperreflexivity.dyadicIncrement line 38
  9. theorem OAI.MarkovSuperreflexivity.norm_dyadicIncrement line 43
  10. theorem OAI.MarkovSuperreflexivity.dyadicIncrement_norm_predictable line 49
  11. theorem OAI.MarkovSuperreflexivity.dyadicIncrement_adapted line 56
  12. theorem OAI.MarkovSuperreflexivity.dyadicIncrement_flip line 64
  13. theorem OAI.MarkovSuperreflexivity.dyadicIncrement_zero_conditional line 69
  14. def OAI.MarkovSuperreflexivity.dyadicProcess line 97
  15. theorem OAI.MarkovSuperreflexivity.dyadicProcess_zero line 102
  16. theorem OAI.MarkovSuperreflexivity.dyadicProcess_difference_succ line 105
  17. theorem OAI.MarkovSuperreflexivity.dyadicProcess_adapted line 112
  18. theorem OAI.MarkovSuperreflexivity.dyadicProcess_isMartingale line 124
  19. theorem OAI.MarkovSuperreflexivity.dyadicProcess_add line 144
  20. theorem OAI.MarkovSuperreflexivity.dyadicProcess_smul line 155
  21. def OAI.MarkovSuperreflexivity.dyadicSynthesis line 167
  22. theorem OAI.MarkovSuperreflexivity.dyadicIncrement_moment line 172
  23. theorem OAI.MarkovSuperreflexivity.dyadicInputMoment_prefixes line 181
  24. theorem OAI.MarkovSuperreflexivity.dyadicInputMoment line 189