OAI/NumberTheory/Jacobsthal/Primes/PrimeTailSplit.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.NumberTheoryLean.InitialPrimeTail.initialConstant line 18
2. theorem OAI.Erdos970.NumberTheoryLean.InitialPrimeTail.initialConstant_pos line 20
3. def OAI.Erdos970.NumberTheoryLean.InitialPrimeTail.initialBudget line 23
4. theorem OAI.Erdos970.NumberTheoryLean.InitialPrimeTail.initialBudget_tendsto_zero line 25
5. theorem OAI.Erdos970.NumberTheoryLean.InitialPrimeTail.initial_tail_integral line 31
6. theorem OAI.Erdos970.NumberTheoryLean.InitialPrimeTail.clean_initial_integral line 37
7. theorem OAI.Erdos970.NumberTheoryLean.InitialPrimeTail.source_initial_tail line 44
8. theorem OAI.Erdos970.NumberTheoryLean.PrimeTailSplit.tail_split_pointwise line 88
9. theorem OAI.Erdos970.NumberTheoryLean.PrimeTailSplit.finite_le_initial_plus_successors line 111
10. theorem OAI.Erdos970.NumberTheoryLean.PrimeTailSplit.add_tail_bounds line 117
11. theorem OAI.Erdos970.NumberTheoryLean.PrimeTailSplit.actual_finite_tail_split line 128