OAI/Analysis/MarkovType/FiniteNormApproximation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MarkovSuperreflexivity.eventually_norm_sub_le_of_pointwise line 22
2. theorem OAI.MarkovSuperreflexivity.exists_scaled_norm_bounds_of_pointwise line 102
3. theorem OAI.MarkovSuperreflexivity.exists_near_isometric_map_of_pointwise line 131