OAI/RingTheory/Interpolation/Bounds.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HahnWilson.Interpolation.budget line 16
2. def OAI.HahnWilson.Interpolation.denominator line 18
3. def OAI.HahnWilson.Interpolation.coefficient line 21
4. def OAI.HahnWilson.Interpolation.moment line 25
5. def OAI.HahnWilson.Interpolation.InPowerIdeal line 29
6. def OAI.HahnWilson.Interpolation.BalancedDistances line 33
7. lemma OAI.HahnWilson.Interpolation.residue_count_le line 37
8. lemma OAI.HahnWilson.Interpolation.residue_others_count_le line 58
9. lemma OAI.HahnWilson.Interpolation.budget_finite_support line 66
10. lemma OAI.HahnWilson.Interpolation.sum_power_div_denominator_integral line 77
11. lemma OAI.HahnWilson.Interpolation.sum_eq_level_counts line 113
12. lemma OAI.HahnWilson.Interpolation.denominator_ne_zero line 128
13. lemma OAI.HahnWilson.Interpolation.denominator_order_le line 134
14. lemma OAI.HahnWilson.Interpolation.quotient_X_pow_integral line 168
15. lemma OAI.HahnWilson.Interpolation.coefficient_integral line 193
16. lemma OAI.HahnWilson.Interpolation.sum_power_div_denominator_small line 200
17. lemma OAI.HahnWilson.Interpolation.moment_eq line 214
18. lemma OAI.HahnWilson.Interpolation.moment_small line 225
19. lemma OAI.HahnWilson.Interpolation.sum_power_div_denominator_scale line 235
20. lemma OAI.HahnWilson.Interpolation.moment_large line 250
21. theorem OAI.HahnWilson.Interpolation.integral_divided_differences line 275