OAI/NumberTheory/Ostmann/Supply/BivariateTruncation.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Supply.BivariateTruncation.coefficientIntegral line 11
2. lemma OAI.Ostmann.Supply.BivariateTruncation.norm_coefficientIntegral_le line 15
3. lemma OAI.Ostmann.Supply.BivariateTruncation.weighted_monomial_eq line 29
4. lemma OAI.Ostmann.Supply.BivariateTruncation.coefficientIntegral_monomial line 36
5. lemma OAI.Ostmann.Supply.BivariateTruncation.weighted_monomial_circleIntegrable line 63
6. lemma OAI.Ostmann.Supply.BivariateTruncation.coefficientIntegral_sum_monomials line 73
7. def OAI.Ostmann.Supply.BivariateTruncation.eval line 86
8. def OAI.Ostmann.Supply.BivariateTruncation.rectangularTruncation line 89
9. lemma OAI.Ostmann.Supply.BivariateTruncation.coefficientIntegral_eval_right line 92
10. lemma OAI.Ostmann.Supply.BivariateTruncation.coefficientIntegral_eval line 104
11. theorem OAI.Ostmann.Supply.BivariateTruncation.coefficient_norm_le line 119
12. lemma OAI.Ostmann.Supply.BivariateTruncation.geometric_pair_sum_le line 133
13. lemma OAI.Ostmann.Supply.BivariateTruncation.geometric_pair_sum_fst_tail_le line 146
14. lemma OAI.Ostmann.Supply.BivariateTruncation.geometric_pair_sum_snd_tail_le line 176
15. lemma OAI.Ostmann.Supply.BivariateTruncation.geometric_rectangular_tail_le line 186
16. lemma OAI.Ostmann.Supply.BivariateTruncation.rectangularTruncation_add_tail line 211
17. theorem OAI.Ostmann.Supply.BivariateTruncation.rectangularTruncation_error_le line 218
18. theorem OAI.Ostmann.Supply.BivariateTruncation.rectangularTruncation_error_le_div line 245