OAI/Analysis/MarkovType/JConvexityBasic.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MarkovSuperreflexivity.cutSign line 19
  2. def OAI.MarkovSuperreflexivity.cutSum line 21
  3. theorem OAI.MarkovSuperreflexivity.abs_cutSign line 24
  4. theorem OAI.MarkovSuperreflexivity.norm_cutSign line 28
  5. theorem OAI.MarkovSuperreflexivity.map_cutSum line 31
  6. theorem OAI.MarkovSuperreflexivity.cutSum_smul line 35
  7. theorem OAI.MarkovSuperreflexivity.cutSum_two_zero line 45
  8. theorem OAI.MarkovSuperreflexivity.cutSum_two_one line 49
  9. def OAI.MarkovSuperreflexivity.JConvexWitness line 53
  10. def OAI.MarkovSuperreflexivity.JConvex line 57
  11. def OAI.MarkovSuperreflexivity.UniformlyNonsquare line 60
  12. def OAI.MarkovSuperreflexivity.AmbientJConvex line 65
  13. theorem OAI.MarkovSuperreflexivity.JConvexWitness.shrink_delta line 68
  14. theorem OAI.MarkovSuperreflexivity.JConvexWitness.comp line 75
  15. theorem OAI.MarkovSuperreflexivity.JConvex.comp line 83
  16. theorem OAI.MarkovSuperreflexivity.JConvexWitness.transport line 88
  17. theorem OAI.MarkovSuperreflexivity.jConvexWitness_two_iff line 105
  18. theorem OAI.MarkovSuperreflexivity.UniformlyNonsquare.jConvex line 128
  19. theorem OAI.MarkovSuperreflexivity.UniformConvex.uniformlyNonsquare line 133
  20. theorem OAI.MarkovSuperreflexivity.UniformConvex.jConvex line 154
  21. theorem OAI.MarkovSuperreflexivity.jConvex_of_subsingleton line 157