OAI/Analysis/MarkovType/UniformSmoothNonsquare.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MarkovSuperreflexivity.seminorm_sub_le line 13
2. theorem OAI.MarkovSuperreflexivity.seminorm_normalize line 17
3. theorem OAI.MarkovSuperreflexivity.seminorm_normalize_error line 22
4. theorem OAI.MarkovSuperreflexivity.unitSphere_nonsquare_of_uniformSmooth line 33
5. theorem OAI.MarkovSuperreflexivity.uniformlyNonsquare_of_unitSphere line 79
6. theorem OAI.MarkovSuperreflexivity.UniformSmooth.uniformlyNonsquare line 131
7. theorem OAI.MarkovSuperreflexivity.UniformSmooth.jConvex line 135