OAI/Analysis/MarkovType/SubdivisionOperators.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MarkovSuperreflexivity.C00.blockOffset line 19
  2. theorem OAI.MarkovSuperreflexivity.C00.blockOffset_zero line 21
  3. theorem OAI.MarkovSuperreflexivity.C00.blockOffset_succ line 24
  4. theorem OAI.MarkovSuperreflexivity.C00.blockOffset_mono line 28
  5. theorem OAI.MarkovSuperreflexivity.C00.blockOffset_strictMono line 34
  6. theorem OAI.MarkovSuperreflexivity.C00.le_blockOffset line 42
  7. theorem OAI.MarkovSuperreflexivity.C00.blockOffset_const line 51
  8. theorem OAI.MarkovSuperreflexivity.C00.blockOffset_mul line 55
  9. theorem OAI.MarkovSuperreflexivity.C00.sum_range_blockOffset line 59
  10. def OAI.MarkovSuperreflexivity.C00.blockIndex line 79
  11. theorem OAI.MarkovSuperreflexivity.C00.blockOffset_le_blockIndex line 82
  12. theorem OAI.MarkovSuperreflexivity.C00.blockIndex_lt_blockOffset_succ line 86
  13. theorem OAI.MarkovSuperreflexivity.C00.blockIndex_injective line 91
  14. theorem OAI.MarkovSuperreflexivity.C00.exists_blockInterval line 114
  15. theorem OAI.MarkovSuperreflexivity.C00.blockIndex_surjective line 132
  16. theorem OAI.MarkovSuperreflexivity.C00.blockIndex_bijective line 142
  17. theorem OAI.MarkovSuperreflexivity.C00.existsUnique_blockIndex line 146
  18. def OAI.MarkovSuperreflexivity.C00.uniformBlockLift line 153
  19. theorem OAI.MarkovSuperreflexivity.C00.uniformBlockLift_apply line 156
  20. theorem OAI.MarkovSuperreflexivity.C00.uniformBlockLift_strictMono line 163
  21. def OAI.MarkovSuperreflexivity.C00.subdivide line 183
  22. def OAI.MarkovSuperreflexivity.C00.uniformSubdivision line 187
  23. theorem OAI.MarkovSuperreflexivity.C00.subdivide_single line 189
  24. theorem OAI.MarkovSuperreflexivity.C00.uniformSubdivision_single line 194
  25. theorem OAI.MarkovSuperreflexivity.C00.subdivide_ofArray line 199
  26. theorem OAI.MarkovSuperreflexivity.C00.subdivide_ofArray_eq_finiteSubdivision line 205
  27. theorem OAI.MarkovSuperreflexivity.C00.subdivide_single_apply_block line 210
  28. theorem OAI.MarkovSuperreflexivity.C00.subdivide_apply_block line 234
  29. theorem OAI.MarkovSuperreflexivity.C00.sum_subdivide_block line 241
  30. theorem OAI.MarkovSuperreflexivity.C00.prefixCut_subdivide line 248
  31. theorem OAI.MarkovSuperreflexivity.C00.subdivide_ofArray_apply_of_ge line 254
  32. def OAI.MarkovSuperreflexivity.C00.l1Mass line 272
  33. theorem OAI.MarkovSuperreflexivity.C00.l1Mass_eq_sum_range line 274
  34. theorem OAI.MarkovSuperreflexivity.C00.l1Mass_ofArray line 285
  35. theorem OAI.MarkovSuperreflexivity.C00.l1Mass_subdivide line 291
  36. theorem OAI.MarkovSuperreflexivity.C00.uniformSubdivision_apply line 304
  37. theorem OAI.MarkovSuperreflexivity.C00.uniformSubdivision_subdivide line 311
  38. theorem OAI.MarkovSuperreflexivity.C00.uniformSubdivision_comp_subdivide line 331
  39. theorem OAI.MarkovSuperreflexivity.C00.uniformSubdivision_mapDomain line 338
  40. theorem OAI.MarkovSuperreflexivity.C00.uniformSubdivision_reindex line 352
  41. theorem OAI.MarkovSuperreflexivity.C00.subdivide_injective line 360
  42. theorem OAI.MarkovSuperreflexivity.C00.prefixCut_uniformSubdivision line 372
  43. theorem OAI.MarkovSuperreflexivity.C00.l1Mass_uniformSubdivision line 378
  44. theorem OAI.MarkovSuperreflexivity.C00.uniformSubdivision_ofArray_apply_of_ge line 382