OAI/NumberTheory/Jacobsthal/Conclusions/JacobsthalSourceScale.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Erdos970.NumberTheoryLean.JacobsthalSourceScale.sourceWline 15 - def
OAI.Erdos970.NumberTheoryLean.JacobsthalSourceScale.sourceBline 16 - theorem
OAI.Erdos970.NumberTheoryLean.JacobsthalSourceScale.log_square_le_sqrt_eventuallyline 18 - theorem
OAI.Erdos970.NumberTheoryLean.JacobsthalSourceScale.sourceW_bounds_eventuallyline 25 - theorem
OAI.Erdos970.NumberTheoryLean.JacobsthalSourceScale.sourceW_tendstoline 40 - theorem
OAI.Erdos970.NumberTheoryLean.JacobsthalSourceScale.source_scale_eventuallyline 46 - theorem
OAI.Erdos970.NumberTheoryLean.JacobsthalSourceScale.sourceB_tendstoline 72 - theorem
OAI.Erdos970.NumberTheoryLean.JacobsthalSourceScale.sourceW_pow_sourceBline 78