OAI/NumberTheory/Ostmann/Construction/NominalTotalsError.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Construction.nominalGapMagnitude line 12
2. def OAI.Ostmann.Construction.nominalGapCoefficient line 15
3. theorem OAI.Ostmann.Construction.nominalGapMagnitude_eq line 19
4. theorem OAI.Ostmann.Construction.nominalGapMagnitude_eventually line 25
5. theorem OAI.Ostmann.Construction.nominalWeight_error_eq line 42
6. theorem OAI.Ostmann.Construction.nominalWeight_error_le line 54
7. theorem OAI.Ostmann.Construction.nominalCompensation_error_eventually line 73