OAI/Analysis/MarkovType/SubdivisionLimit.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MarkovSuperreflexivity.Subdivision.subdivide_le_ofArray line 17
  2. theorem OAI.MarkovSuperreflexivity.Subdivision.subdivide_le line 26
  3. def OAI.MarkovSuperreflexivity.SpreadingModel.subdivisionFamily line 41
  4. theorem OAI.MarkovSuperreflexivity.SpreadingModel.subdivisionFamily_antitone line 44
  5. def OAI.MarkovSuperreflexivity.SpreadingModel.averagedSeminorm line 50
  6. theorem OAI.MarkovSuperreflexivity.SpreadingModel.tendsto_averagedSeminorm line 53
  7. theorem OAI.MarkovSuperreflexivity.SpreadingModel.averaged_le_uniform line 58
  8. theorem OAI.MarkovSuperreflexivity.SpreadingModel.p_le_l1Mass line 67
  9. theorem OAI.MarkovSuperreflexivity.SpreadingModel.subdivisionFamily_upper line 72
  10. theorem OAI.MarkovSuperreflexivity.SpreadingModel.subdivisionFamily_prefix_lower line 78
  11. theorem OAI.MarkovSuperreflexivity.SpreadingModel.averaged_prefix_lower line 84
  12. theorem OAI.MarkovSuperreflexivity.SpreadingModel.averaged_array_upper line 89
  13. theorem OAI.MarkovSuperreflexivity.SpreadingModel.averaged_coordinate_lower line 96
  14. theorem OAI.MarkovSuperreflexivity.SpreadingModel.averaged_definite line 101
  15. theorem OAI.MarkovSuperreflexivity.SpreadingModel.averaged_spreading line 106
  16. theorem OAI.MarkovSuperreflexivity.SpreadingModel.averaged_subdivide line 113