OAI/Analysis/MarkovType/DyadicBellman.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MarkovSuperreflexivity.FiniteDyadicUpperEstimate line 14
  2. def OAI.MarkovSuperreflexivity.dyadicObjective line 17
  3. def OAI.MarkovSuperreflexivity.bellmanValues line 20
  4. def OAI.MarkovSuperreflexivity.bellmanPotential line 23
  5. theorem OAI.MarkovSuperreflexivity.bellmanValues_nonempty line 26
  6. theorem OAI.MarkovSuperreflexivity.bellmanValues_bddAbove line 31
  7. theorem OAI.MarkovSuperreflexivity.dyadicObjective_le_bellman line 41
  8. theorem OAI.MarkovSuperreflexivity.bellmanPotential_bounds line 46
  9. theorem OAI.MarkovSuperreflexivity.bellmanPotential_nonneg line 59
  10. theorem OAI.MarkovSuperreflexivity.bellmanPotential_zero line 64
  11. theorem OAI.MarkovSuperreflexivity.dyadicObjective_scale line 71
  12. theorem OAI.MarkovSuperreflexivity.bellmanPotential_smul line 76
  13. theorem OAI.MarkovSuperreflexivity.norm_rpow_convex line 103
  14. theorem OAI.MarkovSuperreflexivity.moment_translate_convex line 116
  15. theorem OAI.MarkovSuperreflexivity.bellmanPotential_convex line 137
  16. theorem OAI.MarkovSuperreflexivity.exists_dyadicObjective_gt line 169
  17. theorem OAI.MarkovSuperreflexivity.bellmanPotential_add_sub_le line 182