OAI/NumberTheory/Jacobsthal/Estimates/PairedDeficitPositivity.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.NumberTheoryLean.PairedDeficitPositivity.mass_lower_bound line 17
2. theorem OAI.Erdos970.NumberTheoryLean.PairedDeficitPositivity.feedback_lower_bound_upto line 38
3. theorem OAI.Erdos970.NumberTheoryLean.PairedDeficitPositivity.feedback_lower_bound line 61
4. theorem OAI.Erdos970.NumberTheoryLean.PairedDeficitPositivity.feedback_not_tendsto_zero line 70
5. theorem OAI.Erdos970.NumberTheoryLean.PairedDeficitPositivity.first_zero_of_nonpos line 117
6. theorem OAI.Erdos970.NumberTheoryLean.PairedDeficitPositivity.no_first_zero line 146
7. theorem OAI.Erdos970.NumberTheoryLean.PairedDeficitPositivity.paired_pos line 181