OAI/Analysis/MarkovType/PrefixBlocks.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MarkovSuperreflexivity.prefixBlocks_prefixCut_add line 16
  2. theorem OAI.MarkovSuperreflexivity.prefixBlocks_prefixCut_smul line 20
  3. theorem OAI.MarkovSuperreflexivity.sum_Ico_eq_prefixCut_sub line 24
  4. theorem OAI.MarkovSuperreflexivity.prefixCut_single line 28
  5. def OAI.MarkovSuperreflexivity.blockIndex line 45
  6. theorem OAI.MarkovSuperreflexivity.blockIndex_monotone line 48
  7. theorem OAI.MarkovSuperreflexivity.lt_blockIndex_iff line 57
  8. theorem OAI.MarkovSuperreflexivity.blockIndex_lt_iff line 94
  9. theorem OAI.MarkovSuperreflexivity.blockIndex_eq_iff line 103
  10. theorem OAI.MarkovSuperreflexivity.C00.ofArray_apply_ge line 114
  11. def OAI.MarkovSuperreflexivity.prefixBlockCoeffs line 126
  12. def OAI.MarkovSuperreflexivity.prefixBlocksLinear line 138
  13. theorem OAI.MarkovSuperreflexivity.prefixBlocksLinear_apply line 141
  14. theorem OAI.MarkovSuperreflexivity.prefixBlocksLinear_single line 146
  15. theorem OAI.MarkovSuperreflexivity.prefixBlocks_eq_mapDomain line 181
  16. theorem OAI.MarkovSuperreflexivity.OrderedNorm.prefixBlocks_le line 210
  17. theorem OAI.MarkovSuperreflexivity.OrderedNorm.prefixBlocks_le_of_last_eq line 218
  18. theorem OAI.MarkovSuperreflexivity.OrderedNorm.consecutiveBlocks_le line 226