OAI/NumberTheory/Jacobsthal/Primes/PrimeLaw.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.EulerPrimeLaw.incrementProbability line 14
  2. def OAI.Erdos970.EulerPrimeLaw.geometricMass line 15
  3. def OAI.Erdos970.EulerPrimeLaw.bernoulliMass line 16
  4. def OAI.Erdos970.EulerPrimeLaw.eulerMass line 18
  5. abbrev OAI.Erdos970.EulerPrimeLaw.Sample line 22
  6. def OAI.Erdos970.EulerPrimeLaw.jointMass line 23
  7. def OAI.Erdos970.EulerPrimeLaw.lowerExponent line 25
  8. def OAI.Erdos970.EulerPrimeLaw.upperExponent line 26
  9. lemma OAI.Erdos970.EulerPrimeLaw.reciprocal_nonneg line 31
  10. lemma OAI.Erdos970.EulerPrimeLaw.reciprocal_lt_one line 32
  11. lemma OAI.Erdos970.EulerPrimeLaw.incrementProbability_nonneg line 34
  12. lemma OAI.Erdos970.EulerPrimeLaw.incrementProbability_le_one line 37
  13. lemma OAI.Erdos970.EulerPrimeLaw.geometricMass_nonneg line 41
  14. lemma OAI.Erdos970.EulerPrimeLaw.bernoulliMass_nonneg line 44
  15. lemma OAI.Erdos970.EulerPrimeLaw.jointMass_nonneg line 48
  16. lemma OAI.Erdos970.EulerPrimeLaw.eulerMass_nonneg line 50
  17. theorem OAI.Erdos970.EulerPrimeLaw.geometricMass_hasSum line 55
  18. lemma OAI.Erdos970.EulerPrimeLaw.bernoulliMass_hasSum line 63
  19. lemma OAI.Erdos970.EulerPrimeLaw.jointMass_summable line 67
  20. theorem OAI.Erdos970.EulerPrimeLaw.jointMass_hasSum line 71
  21. lemma OAI.Erdos970.EulerPrimeLaw.event_summable line 77
  22. theorem OAI.Erdos970.EulerPrimeLaw.lowerExponent_marginal line 83
  23. lemma OAI.Erdos970.EulerPrimeLaw.zero_convolution line 91
  24. lemma OAI.Erdos970.EulerPrimeLaw.succ_convolution line 99
  25. theorem OAI.Erdos970.EulerPrimeLaw.upperExponent_marginal line 109
  26. theorem OAI.Erdos970.EulerPrimeLaw.eulerMass_hasSum line 123
  27. theorem OAI.Erdos970.EulerPrimeLaw.bernoulli_marginal line 137
  28. lemma OAI.Erdos970.EulerPrimeLaw.weighted_log_excess line 150
  29. lemma OAI.Erdos970.EulerPrimeLaw.log_excess_summable line 156
  30. theorem OAI.Erdos970.EulerPrimeLaw.expected_log_excess line 169
  31. theorem OAI.Erdos970.EulerPrimeLaw.lowerExponent_le_upperExponent line 181
  32. theorem OAI.Erdos970.EulerPrimeLaw.at_two line 186