OAI/NumberTheory/Jacobsthal/Probability/UniformMoment.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.EulerPrimeLaw.log_excess_le_rpow line 12
  2. def OAI.Erdos970.EulerPrimeLaw.integerLogMoment line 28
  3. lemma OAI.Erdos970.EulerPrimeLaw.integerLogMoment_nonneg line 30
  4. lemma OAI.Erdos970.EulerPrimeLaw.integerLogMoment_le line 37
  5. theorem OAI.Erdos970.EulerPrimeLaw.integerLogMoment_summable line 42
  6. def OAI.Erdos970.EulerPrimeLaw.uniformMomentBound line 48
  7. theorem OAI.Erdos970.EulerPrimeLaw.uniformMomentBound_pos line 50
  8. theorem OAI.Erdos970.EulerPrimeLaw.finite_log_moment_le line 55
  9. theorem OAI.Erdos970.EulerPrimeLaw.finite_expected_log_excess_le line 61