OAI/NumberTheory/Ostmann/Arithmetic/HistorySelectedPairDerivativeBoundsNumerics.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Arithmetic.HistorySelectedPairDerivativeBounds.coreExponent line 12
2. lemma OAI.Ostmann.Arithmetic.HistorySelectedPairDerivativeBounds.coreExponent_pos line 15
3. def OAI.Ostmann.Arithmetic.HistorySelectedPairDerivativeBounds.pairExponent line 20
4. lemma OAI.Ostmann.Arithmetic.HistorySelectedPairDerivativeBounds.pairExponent_pos line 23
5. theorem OAI.Ostmann.Arithmetic.HistorySelectedPairDerivativeBounds.pairDerivativeBound_le_exp line 29
6. theorem OAI.Ostmann.Arithmetic.HistorySelectedPairDerivativeBounds.correctedPairDerivativeBound_le_exp line 59