OAI/Analysis/MarkovType/FiniteMartingaleBasic.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MarkovSuperreflexivity.finiteDifference line 21
  2. theorem OAI.MarkovSuperreflexivity.finiteDifference_zero line 25
  3. theorem OAI.MarkovSuperreflexivity.finiteDifference_succ line 30
  4. theorem OAI.MarkovSuperreflexivity.finiteDifference_telescope line 34
  5. def OAI.MarkovSuperreflexivity.HasZeroConditionalSum line 43
  6. theorem OAI.MarkovSuperreflexivity.hasZeroConditionalSum_zero line 46
  7. theorem OAI.MarkovSuperreflexivity.HasZeroConditionalSum.add line 52
  8. theorem OAI.MarkovSuperreflexivity.HasZeroConditionalSum.predictable_smul line 67
  9. theorem OAI.MarkovSuperreflexivity.HasZeroConditionalSum.indicator line 84
  10. def OAI.MarkovSuperreflexivity.FinitePartitionFiltration.IsMartingaleUpTo line 96
  11. theorem OAI.MarkovSuperreflexivity.FinitePartitionFiltration.IsMartingaleUpTo.mono line 102
  12. theorem OAI.MarkovSuperreflexivity.FinitePartitionFiltration.IsMartingaleUpTo.difference_adapted line 108
  13. def OAI.MarkovSuperreflexivity.finiteL2Norm line 123
  14. theorem OAI.MarkovSuperreflexivity.finiteL2Norm_nonneg line 127
  15. theorem OAI.MarkovSuperreflexivity.finiteL2Norm_zero line 131
  16. theorem OAI.MarkovSuperreflexivity.finiteL2Norm_sq line 136
  17. def OAI.MarkovSuperreflexivity.FiniteUpperL2 line 140
  18. def OAI.MarkovSuperreflexivity.FiniteLowerL2 line 148