OAI/Analysis/MarkovType/DyadicConvexPotential.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MarkovSuperreflexivity.FiniteDyadicCotype line 15
  2. def OAI.MarkovSuperreflexivity.DyadicConvex.cost line 25
  3. def OAI.MarkovSuperreflexivity.DyadicConvex.values line 28
  4. def OAI.MarkovSuperreflexivity.DyadicConvex.potential line 31
  5. theorem OAI.MarkovSuperreflexivity.DyadicConvex.values_nonempty line 34
  6. theorem OAI.MarkovSuperreflexivity.DyadicConvex.cost_leaf line 37
  7. theorem OAI.MarkovSuperreflexivity.DyadicConvex.cost_node line 40
  8. theorem OAI.MarkovSuperreflexivity.DyadicConvex.cost_scale line 46
  9. theorem OAI.MarkovSuperreflexivity.DyadicConvex.root_add_energy_le line 51
  10. theorem OAI.MarkovSuperreflexivity.DyadicConvex.cost_lower line 63
  11. theorem OAI.MarkovSuperreflexivity.DyadicConvex.values_bddBelow line 72
  12. theorem OAI.MarkovSuperreflexivity.DyadicConvex.potential_lower line 78
  13. theorem OAI.MarkovSuperreflexivity.DyadicConvex.potential_le_cost line 85
  14. theorem OAI.MarkovSuperreflexivity.DyadicConvex.potential_upper line 90
  15. theorem OAI.MarkovSuperreflexivity.DyadicConvex.potential_nonneg line 95
  16. theorem OAI.MarkovSuperreflexivity.DyadicConvex.potential_zero line 100
  17. theorem OAI.MarkovSuperreflexivity.DyadicConvex.exists_cost_lt line 105
  18. theorem OAI.MarkovSuperreflexivity.DyadicConvex.potential_midpoint line 112
  19. theorem OAI.MarkovSuperreflexivity.DyadicConvex.potential_convex line 139
  20. theorem OAI.MarkovSuperreflexivity.DyadicConvex.potential_scale_le line 149
  21. theorem OAI.MarkovSuperreflexivity.DyadicConvex.potential_homogeneous line 162
  22. def OAI.MarkovSuperreflexivity.DyadicConvex.seminorm line 178
  23. theorem OAI.MarkovSuperreflexivity.DyadicConvex.seminorm_rpow line 183
  24. theorem OAI.MarkovSuperreflexivity.DyadicConvex.seminorm_upper line 188
  25. theorem OAI.MarkovSuperreflexivity.DyadicConvex.seminorm_lower line 193
  26. def OAI.MarkovSuperreflexivity.DyadicConvex.equivalentNorm line 204
  27. theorem OAI.MarkovSuperreflexivity.DyadicConvex.seminorm_symmetric_original line 214
  28. theorem OAI.MarkovSuperreflexivity.DyadicConvex.seminorm_symmetric line 224
  29. theorem OAI.MarkovSuperreflexivity.DyadicConvex.equivalentNorm_uniformConvex line 235
  30. theorem OAI.MarkovSuperreflexivity.hasEquivalentUCNorm_of_finiteDyadicCotype line 246