OAI/NumberTheory/Jacobsthal/Analysis/BonferroniDensity.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.NumberTheoryLean.BonferroniDensity.elementarySum line 17
  2. theorem OAI.Erdos970.NumberTheoryLean.BonferroniDensity.elementarySum_zero line 20
  3. theorem OAI.Erdos970.NumberTheoryLean.BonferroniDensity.elementarySum_nonneg line 23
  4. theorem OAI.Erdos970.NumberTheoryLean.BonferroniDensity.elementarySum_insert line 29
  5. theorem OAI.Erdos970.NumberTheoryLean.BonferroniDensity.factorial_mul_elementarySum_le line 51
  6. theorem OAI.Erdos970.NumberTheoryLean.BonferroniDensity.elementarySum_le_pow_div_factorial line 93
  7. theorem OAI.Erdos970.NumberTheoryLean.BonferroniDensity.elementarySum_le_exponential line 104
  8. theorem OAI.Erdos970.NumberTheoryLean.BonferroniDensity.exp_neg_three_mul_le_eulerProduct line 116
  9. theorem OAI.Erdos970.NumberTheoryLean.BonferroniDensity.relative_elementarySum_le_exponential line 137
  10. theorem OAI.Erdos970.NumberTheoryLean.BonferroniDensity.relative_elementarySum_le_exp_decay line 155
  11. theorem OAI.Erdos970.NumberTheoryLean.BonferroniDensity.prime_density_le_two_thirds line 168
  12. def OAI.Erdos970.NumberTheoryLean.BonferroniDensity.densityPolynomial line 180
  13. theorem OAI.Erdos970.NumberTheoryLean.BonferroniDensity.densityPolynomial_zero line 183
  14. theorem OAI.Erdos970.NumberTheoryLean.BonferroniDensity.densityPolynomial_succ line 186
  15. theorem OAI.Erdos970.NumberTheoryLean.BonferroniDensity.densityPolynomial_empty line 191
  16. theorem OAI.Erdos970.NumberTheoryLean.BonferroniDensity.densityPolynomial_insert line 201
  17. theorem OAI.Erdos970.NumberTheoryLean.BonferroniDensity.densityPolynomial_bounds line 217
  18. theorem OAI.Erdos970.NumberTheoryLean.BonferroniDensity.densityPolynomial_gap line 250
  19. theorem OAI.Erdos970.NumberTheoryLean.BonferroniDensity.densityPolynomial_relative_error line 257
  20. theorem OAI.Erdos970.NumberTheoryLean.BonferroniDensity.densityPolynomial_eq_momentPolynomial line 294
  21. theorem OAI.Erdos970.NumberTheoryLean.BonferroniDensity.prime_densityPolynomial_relative_exp_decay line 297