OAI/NumberTheory/Ostmann/Characters/TemplateOneSidedCancellationProfileBudgetBasic.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Ostmann.Characters.TemplateOneSidedCancellation.historyPolynomialCost_mono_coefficient line 13
2. lemma OAI.Ostmann.Characters.TemplateOneSidedCancellation.linear_le_exp_quartic_cost line 17
3. lemma OAI.Ostmann.Characters.TemplateOneSidedCancellation.constant_mul_exp_quartic_cost line 29
4. lemma OAI.Ostmann.Characters.TemplateOneSidedCancellation.coarseProfile_width_le line 37
5. lemma OAI.Ostmann.Characters.TemplateOneSidedCancellation.normalizedProfile_width_eq line 47