OAI/NumberTheory/Catalan/Estimates/ManuscriptCaseTwoNormAddedRounding.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.InternalCatalan.manuscriptNormPRoundedSubstituteRat line 11
2. theorem OAI.InternalCatalan.manuscriptNormPRoundedSubstitute_error line 23
3. def OAI.InternalCatalan.manuscriptNormVRoundedSubstituteRat line 61
4. theorem OAI.InternalCatalan.manuscriptNormVRoundedSubstitute_error line 76
5. def OAI.InternalCatalan.manuscriptCase2NormRoundedSubstituteRat line 123
6. theorem OAI.InternalCatalan.manuscript_case2_norm_added_rounding_error_le line 129
7. theorem OAI.InternalCatalan.manuscript_case2_norm_added_rounding_error line 142