OAI/Analysis/MarkovType/FiniteConditionalMartingale.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MarkovSuperreflexivity.FinitePartitionFiltration.quotientCoarsening line 19
  2. theorem OAI.MarkovSuperreflexivity.FinitePartitionFiltration.quotientCoarsening_mk line 24
  3. theorem OAI.MarkovSuperreflexivity.FinitePartitionFiltration.quotientCoarsening_comp line 28
  4. def OAI.MarkovSuperreflexivity.FinitePartitionFiltration.conditionalProcess line 34
  5. theorem OAI.MarkovSuperreflexivity.FinitePartitionFiltration.adaptedAt_conditionalProcess line 37
  6. theorem OAI.MarkovSuperreflexivity.FinitePartitionFiltration.fiberSum_conditionalProcess line 43
  7. theorem OAI.MarkovSuperreflexivity.FinitePartitionFiltration.conditionalAverage_conditionalProcess line 52
  8. theorem OAI.MarkovSuperreflexivity.FinitePartitionFiltration.atom_sum_conditionalProcess line 60
  9. theorem OAI.MarkovSuperreflexivity.FinitePartitionFiltration.hasZeroConditionalSum_conditionalProcess_sub line 69
  10. theorem OAI.MarkovSuperreflexivity.FinitePartitionFiltration.isMartingaleUpTo_conditionalProcess line 88
  11. theorem OAI.MarkovSuperreflexivity.FinitePartitionFiltration.finiteL2Norm_conditionalProcess_le line 97