OAI/NumberTheory/JointDickman/Arithmetic/PrimeIndicatorViolations.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Actual prefix and tail violation probabilities

  1. theorem OAI.JointDickman.primePrefix_of_subset line 12
  2. theorem OAI.JointDickman.primeTail_of_subset line 16
  3. theorem OAI.JointDickman.bernoulli_strict_lower_tail line 22
  4. theorem OAI.JointDickman.bernoulli_strict_upper_tail line 48
  5. theorem OAI.JointDickman.bernoulli_prefix_lower_bound line 69
  6. theorem OAI.JointDickman.bernoulli_prefix_upper_bound line 93
  7. theorem OAI.JointDickman.bernoulli_tail_violation_bound line 117