OAI/Analysis/MarkovType/DyadicIndependentBlocks.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MarkovSuperreflexivity.dyadicIndependentBlocks line 14
  2. theorem OAI.MarkovSuperreflexivity.dyadicIndependentBlocks_root line 20
  3. theorem OAI.MarkovSuperreflexivity.dyadicIndependentBlocks_increment line 23
  4. theorem OAI.MarkovSuperreflexivity.dyadicIndependentBlocks_increment_pair line 37
  5. theorem OAI.MarkovSuperreflexivity.dyadicIndependentBlocks_increment_moment line 44
  6. theorem OAI.MarkovSuperreflexivity.dyadicIndependentBlocks_inputMoment line 59
  7. theorem OAI.MarkovSuperreflexivity.dyadicIndependentBlocks_process line 74
  8. theorem OAI.MarkovSuperreflexivity.dyadicIndependentBlocks_boundary line 100
  9. theorem OAI.MarkovSuperreflexivity.dyadicIndependentBlocks_copy_norm_le line 110
  10. def OAI.MarkovSuperreflexivity.dyadicCopyScale line 126
  11. theorem OAI.MarkovSuperreflexivity.dyadicCopyScale_pos line 128
  12. theorem OAI.MarkovSuperreflexivity.dyadicCopyScale_moment line 131
  13. theorem OAI.MarkovSuperreflexivity.dyadicIndependentBlocks_normalized line 138