OAI/Analysis/MarkovType/DyadicTree.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.MarkovSuperreflexivity.DyadicTree line 13
  2. def OAI.MarkovSuperreflexivity.DyadicTree.terminal line 21
  3. theorem OAI.MarkovSuperreflexivity.DyadicTree.terminal_leaf line 26
  4. theorem OAI.MarkovSuperreflexivity.DyadicTree.terminal_node line 29
  5. theorem OAI.MarkovSuperreflexivity.DyadicTree.terminal_mono line 32
  6. theorem OAI.MarkovSuperreflexivity.DyadicTree.terminal_const line 38
  7. theorem OAI.MarkovSuperreflexivity.DyadicTree.terminal_linear line 44
  8. def OAI.MarkovSuperreflexivity.DyadicTree.height line 51
  9. def OAI.MarkovSuperreflexivity.DyadicTree.Full line 55
  10. def OAI.MarkovSuperreflexivity.DyadicTree.pad line 61
  11. theorem OAI.MarkovSuperreflexivity.DyadicTree.pad_full line 66
  12. theorem OAI.MarkovSuperreflexivity.DyadicTree.terminal_pad line 82
  13. def OAI.MarkovSuperreflexivity.DyadicTree.root line 93
  14. theorem OAI.MarkovSuperreflexivity.DyadicTree.root_leaf line 97
  15. theorem OAI.MarkovSuperreflexivity.DyadicTree.root_node line 99
  16. def OAI.MarkovSuperreflexivity.DyadicTree.moment line 102
  17. theorem OAI.MarkovSuperreflexivity.DyadicTree.moment_leaf line 106
  18. theorem OAI.MarkovSuperreflexivity.DyadicTree.moment_node line 109
  19. def OAI.MarkovSuperreflexivity.DyadicTree.energy line 112
  20. theorem OAI.MarkovSuperreflexivity.DyadicTree.energy_leaf line 117
  21. theorem OAI.MarkovSuperreflexivity.DyadicTree.energy_node line 119
  22. theorem OAI.MarkovSuperreflexivity.DyadicTree.moment_nonneg line 124
  23. theorem OAI.MarkovSuperreflexivity.DyadicTree.energy_nonneg line 128
  24. def OAI.MarkovSuperreflexivity.DyadicTree.translate line 135
  25. def OAI.MarkovSuperreflexivity.DyadicTree.scale line 139
  26. theorem OAI.MarkovSuperreflexivity.DyadicTree.root_translate line 143
  27. theorem OAI.MarkovSuperreflexivity.DyadicTree.root_scale line 149
  28. theorem OAI.MarkovSuperreflexivity.DyadicTree.scale_scale line 155
  29. theorem OAI.MarkovSuperreflexivity.DyadicTree.scale_one line 161
  30. theorem OAI.MarkovSuperreflexivity.DyadicTree.terminal_translate line 167
  31. theorem OAI.MarkovSuperreflexivity.DyadicTree.translate_translate line 174
  32. theorem OAI.MarkovSuperreflexivity.DyadicTree.translate_zero line 181
  33. theorem OAI.MarkovSuperreflexivity.DyadicTree.energy_translate line 186
  34. theorem OAI.MarkovSuperreflexivity.DyadicTree.moment_scale line 194
  35. theorem OAI.MarkovSuperreflexivity.DyadicTree.energy_scale line 202
  36. theorem OAI.MarkovSuperreflexivity.DyadicTree.root_pad line 214
  37. theorem OAI.MarkovSuperreflexivity.DyadicTree.moment_pad line 223
  38. theorem OAI.MarkovSuperreflexivity.DyadicTree.energy_pad line 226