OAI/Combinatorics/Progressions/Dynamics/AllocatedExternalCandidateReturnedModulusBudget.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.retainedPatchModulusLog_le_cubic line 11
2. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.referenceRetainedCRTModulus_le_exp_discount line 79
3. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.Conclusion.returned_modulus_le_exp_discount line 162