OAI/Combinatorics/BalancedRyser/Probability/PatternMomentsLemmas.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Balanced.PatternModel line 15
  2. abbrev OAI.Balanced.PatternModel.Sample line 35
  3. def OAI.Balanced.PatternModel.measure line 37
  4. def OAI.Balanced.PatternModel.fixCoordinates line 39
  5. def OAI.Balanced.PatternModel.indicator line 44
  6. def OAI.Balanced.PatternModel.count line 47
  7. def OAI.Balanced.PatternModel.fixedExpectation line 50
  8. def OAI.Balanced.PatternModel.overlapCount line 54
  9. def OAI.Balanced.UniformPatternSupports line 61
  10. def OAI.Balanced.BoundedInitialColors line 64
  11. def OAI.Balanced.UniformPatternTotalBound line 68
  12. def OAI.Balanced.UniformPatternOverlapBound line 74
  13. def OAI.Balanced.UniformPatternMoments line 80
  14. def OAI.Balanced.UniformCenteredPatternMoments line 86
  15. def OAI.Balanced.PatternMomentsResult line 94
  16. theorem OAI.Balanced.ConditionalFailure.joint_eq_cond_mul line 113
  17. theorem OAI.Balanced.ConditionalFailure.joint_le_cond line 120
  18. theorem OAI.Balanced.ConditionalFailure.cond_le_joint_div line 127
  19. theorem OAI.Balanced.ConditionalFailure.tendsto_joint_zero_of_cond line 136
  20. theorem OAI.Balanced.ConditionalFailure.tendsto_cond_zero_of_joint line 145
  21. theorem OAI.Balanced.ConditionalFailure.joint_preimage_eq_map_cond_mul line 157
  22. theorem OAI.Balanced.ConditionalFailure.tendsto_joint_preimage_zero_of_map_cond line 166
  23. theorem OAI.Balanced.PatternExposureKernel.lmarginal_idempotent line 195
  24. theorem OAI.Balanced.PatternExposureKernel.lmarginal_tower line 209
  25. theorem OAI.Balanced.PatternExposureKernel.exposure_tower line 215
  26. theorem OAI.Balanced.PatternExposureKernel.lintegral_lmarginal line 224
  27. theorem OAI.Balanced.inv_one_sub_le_exp_two_mul line 241
  28. theorem OAI.Balanced.avoidance_prod_pos line 249
  29. theorem OAI.Balanced.one_sub_sum_le_avoidance_prod line 254
  30. theorem OAI.Balanced.prod_inv_one_sub_le_exp_two_sum line 270
  31. theorem OAI.Balanced.prod_inv_one_sub_le_exp_half line 283