OAI/Analysis/MarkovType/FiniteL2CoefficientAdapter.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MarkovSuperreflexivity.finiteL2ToSequence line 18
  2. theorem OAI.MarkovSuperreflexivity.finiteL2ToSequence_norm_sq line 32
  3. theorem OAI.MarkovSuperreflexivity.finiteL2ToSequence_norm line 59
  4. theorem OAI.MarkovSuperreflexivity.finiteL2ToSequence_eq_zero_on_mass_pos line 64
  5. theorem OAI.MarkovSuperreflexivity.finiteL2Norm_eq_of_positive_mass line 75
  6. theorem OAI.MarkovSuperreflexivity.FinitePartitionFiltration.IsMartingaleUpTo.finiteL2Norm_le_terminal line 86
  7. def OAI.MarkovSuperreflexivity.finiteCoefficientProcess line 98
  8. theorem OAI.MarkovSuperreflexivity.finiteCoefficientProcess_terminal line 103
  9. theorem OAI.MarkovSuperreflexivity.finiteCoefficientProcess_difference line 111
  10. theorem OAI.MarkovSuperreflexivity.finiteCoefficientProcess_isMartingale line 133
  11. theorem OAI.MarkovSuperreflexivity.finiteDifference_coefficientMonotone line 155
  12. theorem OAI.MarkovSuperreflexivity.sum_finiteL2ToSequence_differences line 194
  13. theorem OAI.MarkovSuperreflexivity.finiteLowerL2_of_sequence_obstruction line 206