OAI/Analysis/MarkovType/FiniteMartingalePairing.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MarkovSuperreflexivity.FiniteLaw.expect_pair_key_right_clm line 19
  2. theorem OAI.MarkovSuperreflexivity.FiniteLaw.expect_pair_key_left_clm line 30
  3. theorem OAI.MarkovSuperreflexivity.FiniteLaw.expect_pair_conditionalAverage_clm line 40
  4. theorem OAI.MarkovSuperreflexivity.FinitePartitionFiltration.expect_pair_conditionalProcess_of_adapted line 55
  5. theorem OAI.MarkovSuperreflexivity.HasZeroConditionalSum.expect_pair_of_atom_constant line 76
  6. theorem OAI.MarkovSuperreflexivity.sum_finiteDifference_eq line 95
  7. theorem OAI.MarkovSuperreflexivity.finite_martingale_difference_pairing line 105
  8. theorem OAI.MarkovSuperreflexivity.finite_martingale_terminal_pairing line 133