OAI/Analysis/MarkovType/SubdivisionNearIsometry.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MarkovSuperreflexivity.C00.uniformArrayMap line 15
2. theorem OAI.MarkovSuperreflexivity.C00.ofArray_uniformArrayMap line 28
3. theorem OAI.MarkovSuperreflexivity.SpreadingModel.averaged_array_norm_lower line 39
4. theorem OAI.MarkovSuperreflexivity.SpreadingModel.subdivisionFamily_array_norm_upper line 51
5. theorem OAI.MarkovSuperreflexivity.SpreadingModel.exists_uniform_nearIsometry line 60