OAI/NumberTheory/Jacobsthal/Analysis/ContinuousHighRemoval.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Erdos970.ErdosPrimeInputs.ContinuousHighRemoval.tail_coefficient_eq line 16
2. lemma OAI.Erdos970.ErdosPrimeInputs.ContinuousHighRemoval.tail_coefficient_bound line 25
3. lemma OAI.Erdos970.ErdosPrimeInputs.ContinuousHighRemoval.reward_coefficient_bound line 41
4. lemma OAI.Erdos970.ErdosPrimeInputs.ContinuousHighRemoval.tail_saving line 56
5. lemma OAI.Erdos970.ErdosPrimeInputs.ContinuousHighRemoval.gap_saving line 61
6. theorem OAI.Erdos970.ErdosPrimeInputs.ContinuousHighRemoval.low_gap_high_removal line 65
7. theorem OAI.Erdos970.ErdosPrimeInputs.ContinuousHighRemoval.rewarded_high_removal line 88