OAI/Analysis/MarkovType/SubdivisionOrderedNorm.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MarkovSuperreflexivity.SpreadingModel.averaged_mergeAt line 16
2. def OAI.MarkovSuperreflexivity.SpreadingModel.orderedNorm line 30
3. theorem OAI.MarkovSuperreflexivity.SpreadingModel.orderedNorm_apply line 36
4. theorem OAI.MarkovSuperreflexivity.SpreadingModel.orderedNorm_prefix_lower line 39
5. theorem OAI.MarkovSuperreflexivity.SpreadingModel.orderedNorm_subdivide line 42
6. theorem OAI.MarkovSuperreflexivity.SpreadingModel.orderedNorm_uniformSubdivision line 47
7. theorem OAI.MarkovSuperreflexivity.SpreadingModel.orderedNorm_scaled_uniform line 52
8. theorem OAI.MarkovSuperreflexivity.SpreadingModel.orderedNorm_representable line 58
9. theorem OAI.MarkovSuperreflexivity.exists_orderedNorm_of_spreadingModel line 68