OAI/NumberTheory/Ostmann/Characters/HistoryArchimedeanVariationData.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Ostmann.Characters.HistoryPolynomialData line 10
2. def OAI.Ostmann.Characters.HistoryPolynomialData.weight line 21
3. def OAI.Ostmann.Characters.HistoryPolynomialData.degreeCost line 24
4. structure OAI.Ostmann.Characters.HistoryPolynomialData.Ranges line 27
5. def OAI.Ostmann.Characters.HistoryPolynomialData.variationCost line 38
6. theorem OAI.Ostmann.Characters.HistoryPolynomialData.variationCost_nonneg line 41
7. theorem OAI.Ostmann.Characters.HistoryPolynomialData.progressionVariation_le line 46
8. theorem OAI.Ostmann.Characters.HistoryPolynomialData.scaled_progressionVariation_le line 55