OAI/NumberTheory/Jacobsthal/Primes/BoundaryPrimeMass.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.NumberTheoryLean.VariablePrimeTilt.variable_tilt_weight line 16
2. theorem OAI.Erdos970.NumberTheoryLean.VariablePrimeTilt.long_prefix_variable_tilt line 25
3. def OAI.Erdos970.NumberTheoryLean.VariablePrimeTilt.omissionMass line 50
4. theorem OAI.Erdos970.NumberTheoryLean.VariablePrimeTilt.omission_mass_le_long line 53
5. theorem OAI.Erdos970.NumberTheoryLean.VariablePrimeTilt.actual_omission_variable_tilt line 69
6. theorem OAI.Erdos970.NumberTheoryLean.BoundaryPrimeMass.prime_sum_le_prefix_mass line 85
7. theorem OAI.Erdos970.NumberTheoryLean.BoundaryPrimeMass.uniform_boundary_mass line 105