OAI/Analysis/MarkovType/DyadicTreeMartingale.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MarkovSuperreflexivity.dyadicLaw_expect_snoc line 15
  2. theorem OAI.MarkovSuperreflexivity.FiniteLaw.vexpect_const line 30
  3. theorem OAI.MarkovSuperreflexivity.dyadicLaw_vexpect_snoc line 34
  4. def OAI.MarkovSuperreflexivity.DyadicTree.branch line 51
  5. def OAI.MarkovSuperreflexivity.DyadicTree.splitCoefficient line 55
  6. def OAI.MarkovSuperreflexivity.DyadicTree.descendant line 59
  7. theorem OAI.MarkovSuperreflexivity.DyadicTree.descendant_zero line 64
  8. theorem OAI.MarkovSuperreflexivity.DyadicTree.descendant_snoc line 68
  9. theorem OAI.MarkovSuperreflexivity.DyadicTree.root_branch line 73
  10. theorem OAI.MarkovSuperreflexivity.DyadicTree.root_branch_average line 77
  11. theorem OAI.MarkovSuperreflexivity.DyadicTree.moment_branch_average line 84
  12. theorem OAI.MarkovSuperreflexivity.DyadicTree.energy_branch_average line 90
  13. theorem OAI.MarkovSuperreflexivity.DyadicTree.full_branch line 98
  14. theorem OAI.MarkovSuperreflexivity.DyadicTree.full_descendant line 107
  15. theorem OAI.MarkovSuperreflexivity.DyadicTree.moment_full_zero line 116
  16. theorem OAI.MarkovSuperreflexivity.DyadicTree.energy_full_zero line 122
  17. theorem OAI.MarkovSuperreflexivity.DyadicTree.vexpect_root_descendant line 128
  18. theorem OAI.MarkovSuperreflexivity.DyadicTree.expect_moment_descendant line 137
  19. theorem OAI.MarkovSuperreflexivity.DyadicTree.expected_energy_step line 146
  20. theorem OAI.MarkovSuperreflexivity.DyadicTree.energy_telescope line 157
  21. def OAI.MarkovSuperreflexivity.DyadicTree.coefficients line 169
  22. theorem OAI.MarkovSuperreflexivity.DyadicTree.coefficients_root line 173
  23. theorem OAI.MarkovSuperreflexivity.DyadicTree.coefficients_prefix line 176
  24. theorem OAI.MarkovSuperreflexivity.DyadicTree.process_coefficients line 180
  25. theorem OAI.MarkovSuperreflexivity.DyadicTree.synthesis_coefficients line 195
  26. theorem OAI.MarkovSuperreflexivity.DyadicTree.process_eq_descendant_average line 201
  27. theorem OAI.MarkovSuperreflexivity.DyadicTree.synthesis_moment line 208
  28. theorem OAI.MarkovSuperreflexivity.DyadicTree.coefficients_energy line 220
  29. theorem OAI.MarkovSuperreflexivity.DyadicTree.coefficients_inputMoment line 233
  30. theorem OAI.MarkovSuperreflexivity.DyadicTree.exists_dyadic_model line 238