OAI/NumberTheory/Jacobsthal/Sieve/UniformExponentialOccupation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.NumberTheoryLean.UniformExponentialOccupation.positiveGapEnvelope line 18
2. def OAI.Erdos970.NumberTheoryLean.UniformExponentialOccupation.exponentialPrefixMass line 20
3. theorem OAI.Erdos970.NumberTheoryLean.UniformExponentialOccupation.envelope_nonneg line 23
4. theorem OAI.Erdos970.NumberTheoryLean.UniformExponentialOccupation.compact_tail_split line 27
5. theorem OAI.Erdos970.NumberTheoryLean.UniformExponentialOccupation.uniform_exponential_prefix_mass line 47
6. theorem OAI.Erdos970.NumberTheoryLean.UniformExponentialOccupation.uniform_signed_exponential_rewards line 70