OAI/Analysis/MarkovType/FiniteMartingaleTransport.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MarkovSuperreflexivity.FiniteLaw.reindex line 18
  2. theorem OAI.MarkovSuperreflexivity.FiniteLaw.reindex_mass line 23
  3. theorem OAI.MarkovSuperreflexivity.FiniteLaw.expect_reindex line 26
  4. theorem OAI.MarkovSuperreflexivity.FiniteLaw.vexpect_reindex line 30
  5. theorem OAI.MarkovSuperreflexivity.FiniteLaw.prob_reindex line 35
  6. def OAI.MarkovSuperreflexivity.FinitePartitionFiltration.reindex line 44
  7. theorem OAI.MarkovSuperreflexivity.FinitePartitionFiltration.AdaptedAt.reindex line 52
  8. theorem OAI.MarkovSuperreflexivity.HasZeroConditionalSum.reindex line 62
  9. theorem OAI.MarkovSuperreflexivity.finiteDifference_comp_equiv line 72
  10. theorem OAI.MarkovSuperreflexivity.finiteL2Norm_reindex line 80
  11. theorem OAI.MarkovSuperreflexivity.FinitePartitionFiltration.IsMartingaleUpTo.reindex line 88
  12. theorem OAI.MarkovSuperreflexivity.FiniteUpperL2.apply line 101
  13. theorem OAI.MarkovSuperreflexivity.FiniteLowerL2.apply line 115