OAI/NumberTheory/Jacobsthal/Estimates/BonferroniBlocks.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.NumberTheoryLean.BonferroniBlocks.alternatingChoose line 15
  2. theorem OAI.Erdos970.NumberTheoryLean.BonferroniBlocks.alternatingChoose_zero line 18
  3. theorem OAI.Erdos970.NumberTheoryLean.BonferroniBlocks.alternatingChoose_succ line 26
  4. theorem OAI.Erdos970.NumberTheoryLean.BonferroniBlocks.alternatingChoose_even_nonneg line 31
  5. theorem OAI.Erdos970.NumberTheoryLean.BonferroniBlocks.alternatingChoose_bounds line 39
  6. theorem OAI.Erdos970.NumberTheoryLean.BonferroniBlocks.alternatingChoose_gap line 52
  7. def OAI.Erdos970.NumberTheoryLean.BonferroniBlocks.hitSet line 60
  8. def OAI.Erdos970.NumberTheoryLean.BonferroniBlocks.intersectionValue line 64
  9. def OAI.Erdos970.NumberTheoryLean.BonferroniBlocks.coefficientPolynomial line 68
  10. def OAI.Erdos970.NumberTheoryLean.BonferroniBlocks.survives line 72
  11. theorem OAI.Erdos970.NumberTheoryLean.BonferroniBlocks.sum_intersectionValue_eq_choose line 76
  12. theorem OAI.Erdos970.NumberTheoryLean.BonferroniBlocks.coefficientPolynomial_eq_alternatingChoose line 93
  13. theorem OAI.Erdos970.NumberTheoryLean.BonferroniBlocks.survives_eq_zero_count line 101
  14. theorem OAI.Erdos970.NumberTheoryLean.BonferroniBlocks.coefficientPolynomial_bounds line 109
  15. theorem OAI.Erdos970.NumberTheoryLean.BonferroniBlocks.coefficientPolynomial_even_nonneg line 116
  16. theorem OAI.Erdos970.NumberTheoryLean.BonferroniBlocks.coefficientPolynomial_gap line 121
  17. theorem OAI.Erdos970.NumberTheoryLean.BonferroniBlocks.coefficientPolynomial_eq_one_of_no_hits line 127
  18. def OAI.Erdos970.NumberTheoryLean.BonferroniBlocks.blockUpper line 134
  19. def OAI.Erdos970.NumberTheoryLean.BonferroniBlocks.blockCorrection line 138
  20. def OAI.Erdos970.NumberTheoryLean.BonferroniBlocks.blockLower line 145
  21. theorem OAI.Erdos970.NumberTheoryLean.BonferroniBlocks.block_bounds line 149
  22. theorem OAI.Erdos970.NumberTheoryLean.BonferroniBlocks.weighted_block_bounds line 212
  23. theorem OAI.Erdos970.NumberTheoryLean.BonferroniBlocks.coefficient_abs line 227
  24. theorem OAI.Erdos970.NumberTheoryLean.BonferroniBlocks.coefficient_divisor_support line 229
  25. def OAI.Erdos970.NumberTheoryLean.BonferroniBlocks.intersectionMass line 241
  26. def OAI.Erdos970.NumberTheoryLean.BonferroniBlocks.momentPolynomial line 245
  27. theorem OAI.Erdos970.NumberTheoryLean.BonferroniBlocks.weighted_polynomial_eq_moments line 248
  28. theorem OAI.Erdos970.NumberTheoryLean.BonferroniBlocks.weighted_single_block_bounds line 264
  29. def OAI.Erdos970.NumberTheoryLean.BonferroniBlocks.intersectionRemainder line 279
  30. theorem OAI.Erdos970.NumberTheoryLean.BonferroniBlocks.momentPolynomial_decomposition line 283
  31. theorem OAI.Erdos970.NumberTheoryLean.BonferroniBlocks.momentPolynomial_abs_le line 298
  32. theorem OAI.Erdos970.NumberTheoryLean.BonferroniBlocks.weighted_single_block_with_remainders line 311