OAI/Combinatorics/BalancedRyser/Candidates/CandidatePairMoments.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.CandidatePairs.pairTotalConstant line 15
  2. def OAI.Balanced.CandidatePairs.pairFirstOverlapConstant line 18
  3. def OAI.Balanced.CandidatePairs.pairExposureConstant line 21
  4. theorem OAI.Balanced.CandidatePairs.pairTotalConstant_nonneg line 24
  5. theorem OAI.Balanced.CandidatePairs.pairFirstOverlapConstant_nonneg line 28
  6. theorem OAI.Balanced.CandidatePairs.pairExposureConstant_nonneg line 32
  7. theorem OAI.Balanced.CandidatePairs.pairPatternModel_total_le line 36
  8. theorem OAI.Balanced.CandidatePairs.pairPatternModel_overlap_le line 47
  9. def OAI.Balanced.CandidatePairs.pairCenteredMomentConstant line 64
  10. theorem OAI.Balanced.CandidatePairs.pairCenteredMomentConstant_nonneg line 68
  11. theorem OAI.Balanced.CandidatePairs.pairPatternModel_centered_moment_le line 74
  12. theorem OAI.Balanced.CandidatePairs.pairCount_centered_moment_le line 90
  13. theorem OAI.Balanced.CandidatePairs.mean_pairCount_le line 101
  14. def OAI.Balanced.CandidatePairs.pairLinearThreshold line 110
  15. theorem OAI.Balanced.CandidatePairs.pairLinearThreshold_pos line 112
  16. theorem OAI.Balanced.CandidatePairs.pairCount_upper_tail line 116
  17. theorem OAI.Balanced.CandidatePairs.pairCount_any_upper_tail line 152
  18. theorem OAI.Balanced.CandidatePairs.rootFiberSquareCount_any_upper_tail line 183