OAI/NumberTheory/Catalan/Polynomial/RawCoefficientEntryBound.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.InternalCatalan.discrepancyNormFactor line 11
2. theorem OAI.InternalCatalan.one_le_discrepancyNormFactor line 14
3. theorem OAI.InternalCatalan.discrepancyNormFactor_nonneg line 17
4. theorem OAI.InternalCatalan.rawCoefficientEntry_norm_le line 20