OAI/Combinatorics/BalancedRyser/Probability/PatternIntegrability.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.Balanced.PatternModel.isProbabilityMeasure_measure line 12
  2. lemma OAI.Balanced.PatternModel.measurable_fixCoordinates line 16
  3. lemma OAI.Balanced.PatternModel.measurable_indicator line 25
  4. lemma OAI.Balanced.PatternModel.indicator_nonneg line 28
  5. lemma OAI.Balanced.PatternModel.indicator_le_one line 33
  6. lemma OAI.Balanced.PatternModel.measurable_count line 38
  7. lemma OAI.Balanced.PatternModel.integrable_fixed_of_bound line 42
  8. lemma OAI.Balanced.PatternModel.integrable_fixed_indicator line 50
  9. lemma OAI.Balanced.PatternModel.fixedExpectation_nonneg line 57
  10. lemma OAI.Balanced.PatternModel.fixedExpectation_const line 61
  11. lemma OAI.Balanced.PatternModel.fixedExpectation_indicator_nonneg line 65
  12. lemma OAI.Balanced.PatternModel.fixedExpectation_indicator_le_one line 69
  13. def OAI.Balanced.PatternModel.positiveProduct line 78
  14. def OAI.Balanced.PatternModel.centeredProduct line 82
  15. def OAI.Balanced.PatternModel.productWeight line 86
  16. lemma OAI.Balanced.PatternModel.positiveProduct_nonneg line 90
  17. lemma OAI.Balanced.PatternModel.positiveProduct_le line 97
  18. lemma OAI.Balanced.PatternModel.measurable_positiveProduct line 109
  19. lemma OAI.Balanced.PatternModel.measurable_centeredProduct line 116
  20. lemma OAI.Balanced.PatternModel.abs_centeredProduct_le line 123
  21. lemma OAI.Balanced.PatternModel.integrable_fixed_positiveProduct line 136
  22. lemma OAI.Balanced.PatternModel.integrable_fixed_centeredProduct line 144
  23. lemma OAI.Balanced.PatternModel.productWeight_nonneg line 151
  24. lemma OAI.Balanced.PatternModel.productWeight_nil line 155
  25. lemma OAI.Balanced.PatternModel.positiveProduct_perm line 160
  26. lemma OAI.Balanced.PatternModel.centeredProduct_perm line 166
  27. lemma OAI.Balanced.PatternModel.productWeight_perm line 172
  28. lemma OAI.Balanced.PatternModel.abs_fixedExpectation_centeredProduct_le line 178
  29. lemma OAI.Balanced.PatternModel.indicator_eq_of_agree line 190
  30. lemma OAI.Balanced.PatternModel.positiveProduct_eq_of_agree line 200
  31. lemma OAI.Balanced.PatternModel.centeredProduct_eq_of_agree line 212
  32. def OAI.Balanced.PatternModel.additionalSupport line 224
  33. lemma OAI.Balanced.PatternModel.positiveProduct_dependsOn line 229
  34. lemma OAI.Balanced.PatternModel.centeredProduct_dependsOn line 243
  35. lemma OAI.Balanced.PatternModel.fixedExpectation_count_eq_sum line 257
  36. lemma OAI.Balanced.PatternModel.sum_centered_indicators line 263