OAI/NumberTheory/Jacobsthal/Estimates/SourceLargePairBound.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.ErdosVarianceLargeCount.finite_large_pair_bound line 16
2. def OAI.Erdos970.ErdosVarianceLargeScale.slowHyperbolaFactor line 71
3. theorem OAI.Erdos970.ErdosVarianceLargeScale.hyperbolaEnvelope_factor line 74
4. theorem OAI.Erdos970.ErdosVarianceLargeScale.source_hyperbola_scales line 79
5. theorem OAI.Erdos970.ErdosVarianceLargeScale.large_error_algebra line 147
6. theorem OAI.Erdos970.ErdosVarianceLargeScale.eventual_large_error_budgets line 217
7. theorem OAI.Erdos970.ErdosVarianceLargeScale.source_large_error line 243
8. theorem OAI.Erdos970.ErdosVarianceLargeScale.source_large_pair_bound line 282