OAI/Combinatorics/BalancedRyser/Probability/CenteredIncrements.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.integrable_of_abs_le line 15
  2. theorem OAI.Balanced.abs_sub_condExp_le line 22
  3. theorem OAI.Balanced.condExp_sub_condExp_eq_zero line 31
  4. theorem OAI.Balanced.integrable_sub_condExp line 40
  5. theorem OAI.Balanced.stronglyMeasurable_centered_increment_of_measurable line 48
  6. theorem OAI.Balanced.stronglyMeasurable_increment line 56
  7. theorem OAI.Balanced.stronglyMeasurable_centered_increment line 62
  8. theorem OAI.Balanced.sum_centered_increments_eq line 68