OAI/NumberTheory/Jacobsthal/Estimates/EndpointSoftConclusion.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.ErdosVarianceEligible.soft_of_not_guarded_hard line 14
2. theorem OAI.Erdos970.ErdosVarianceEligible.soft_guarded_point_eligible line 25
3. theorem OAI.Erdos970.ErdosVarianceEligible.endpoint_soft_conclusion line 50