OAI/Combinatorics/BalancedRyser/Probability/IndependentTrials3.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.IndependentTrials.abs_integral_sub_integral_le line 18
  2. theorem OAI.Balanced.IndependentTrials.abs_sub_integral_le_of_oscillation line 27
  3. theorem OAI.Balanced.IndependentTrials.averaged_oscillation line 34
  4. theorem OAI.Balanced.IndependentTrials.conditional_second_moment_le line 41
  5. theorem OAI.Balanced.IndependentTrials.conditional_variance_eq_second_moment line 49
  6. theorem OAI.Balanced.IndependentTrials.conditional_variance_le_of_centered_bound line 57
  7. theorem OAI.Balanced.IndependentTrials.martingale_increment_condExp_zero line 65
  8. theorem OAI.Balanced.IndependentTrials.martingale_increment_condVar_le line 77
  9. theorem OAI.Balanced.IndependentTrials.prefixIndices_zero line 91
  10. theorem OAI.Balanced.IndependentTrials.prefixIndices_full line 94
  11. theorem OAI.Balanced.IndependentTrials.prefixFiltration_zero line 98
  12. theorem OAI.Balanced.IndependentTrials.piFinset_univ line 111
  13. theorem OAI.Balanced.IndependentTrials.prefixFiltration_full line 123
  14. theorem OAI.Balanced.IndependentTrials.measurable_outcome_full line 128
  15. theorem OAI.Balanced.IndependentTrials.doobProcess_full line 134
  16. theorem OAI.Balanced.IndependentTrials.doobProcess_zero line 142
  17. theorem OAI.Balanced.IndependentTrials.CoordinateOscillation.abs_sub_le_sum line 147
  18. theorem OAI.Balanced.IndependentTrials.CoordinateOscillation.abs_le line 172
  19. theorem OAI.Balanced.IndependentTrials.CoordinateOscillation.integrable_comp line 182