OAI/NumberTheory/Jacobsthal/Primes/LiteralUniformPrimeTail.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.NumberTheoryLean.PrimeFamilyOccupation.removed_signed_reward_bound line 18
  2. theorem OAI.Erdos970.NumberTheoryLean.PrimeFamilyOccupation.removed_signed_reward_every_power line 41
  3. def OAI.Erdos970.NumberTheoryLean.LiteralPrimeOccupation.nodeReward line 71
  4. def OAI.Erdos970.NumberTheoryLean.LiteralPrimeOccupation.familyValue line 74
  5. def OAI.Erdos970.NumberTheoryLean.LiteralPrimeOccupation.sourceFactor line 78
  6. theorem OAI.Erdos970.NumberTheoryLean.LiteralPrimeOccupation.signed_weight_test_identity line 81
  7. theorem OAI.Erdos970.NumberTheoryLean.LiteralPrimeOccupation.literal_corrected_occupation line 95
  8. def OAI.Erdos970.NumberTheoryLean.LiteralPrimeOccupation.tailListReward line 111
  9. theorem OAI.Erdos970.NumberTheoryLean.LiteralPrimeOccupation.tailListReward_nonneg line 114
  10. theorem OAI.Erdos970.NumberTheoryLean.LiteralPrimeOccupation.tail_weight_test_identity line 118
  11. theorem OAI.Erdos970.NumberTheoryLean.LiteralPrimeOccupation.literal_scaled_tail line 130
  12. theorem OAI.Erdos970.NumberTheoryLean.LiteralUniformPrimeTail.tailListReward_envelope line 155
  13. theorem OAI.Erdos970.NumberTheoryLean.LiteralUniformPrimeTail.actual_uniform_original_prime_tail line 162