OAI/NumberTheory/Ostmann/Arithmetic/HistoryGiantXiReplacementActualBoundsBasic.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Ostmann.Arithmetic.HistoryGiantXiReplacementActual.referenceAmplitude_nonneg line 22
2. lemma OAI.Ostmann.Arithmetic.HistoryGiantXiReplacementActual.referenceDerivative_nonneg line 27
3. lemma OAI.Ostmann.Arithmetic.HistoryGiantXiReplacementActual.selected_exp_le_smoothGrowth line 32
4. theorem OAI.Ostmann.Arithmetic.HistoryGiantXiReplacementActual.reference_envelopes line 41
5. lemma OAI.Ostmann.Arithmetic.HistoryGiantXiReplacementActual.prime_grid_card_le line 61
6. lemma OAI.Ostmann.Arithmetic.HistoryGiantXiReplacementActual.mixed_grid_card_le line 70