OAI/NumberTheory/Jacobsthal/Estimates/ScaledOriginalTail.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.NumberTheoryLean.SourceSuccessfulTail.even_source_cost_state line 19
2. theorem OAI.Erdos970.NumberTheoryLean.SourceSuccessfulTail.source_successful_tail line 28
3. def OAI.Erdos970.NumberTheoryLean.SourceTailBudget.failureBudget line 82
4. theorem OAI.Erdos970.NumberTheoryLean.SourceTailBudget.failureBudget_tendsto_zero line 84
5. theorem OAI.Erdos970.NumberTheoryLean.SourceTailBudget.source_tail_budget line 89
6. theorem OAI.Erdos970.NumberTheoryLean.SourceUniformTail.four_quarters line 163
7. theorem OAI.Erdos970.NumberTheoryLean.SourceUniformTail.actual_uniform_inverse_tail line 171
8. def OAI.Erdos970.NumberTheoryLean.ScaledOriginalTail.prefactorBound line 231
9. theorem OAI.Erdos970.NumberTheoryLean.ScaledOriginalTail.prefactorBound_pos line 233
10. def OAI.Erdos970.NumberTheoryLean.ScaledOriginalTail.scaledTail line 236
11. theorem OAI.Erdos970.NumberTheoryLean.ScaledOriginalTail.scaled_reward_prefactor line 241
12. theorem OAI.Erdos970.NumberTheoryLean.ScaledOriginalTail.source_scaled_tail_envelope line 268
13. theorem OAI.Erdos970.NumberTheoryLean.ScaledOriginalTail.actual_uniform_scaled_tail line 295