OAI/Analysis/TriangularHilbert/FiniteLineMax.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TriangularHilbert.lineExtend line 12
2. lemma OAI.TriangularHilbert.lineExtend_apply line 15
3. lemma OAI.TriangularHilbert.sum_lineExtend line 18
4. def OAI.TriangularHilbert.lineMax line 23
5. lemma OAI.TriangularHilbert.lineMax_nonneg line 25
6. lemma OAI.TriangularHilbert.lineMax_strong line 29
7. lemma OAI.TriangularHilbert.gaussian_sum_le_lineMax line 40
8. lemma OAI.TriangularHilbert.cubic_young line 48
9. lemma OAI.TriangularHilbert.sum_abs_sq_sqrt line 57
10. lemma OAI.TriangularHilbert.lineMax_scalar_product_bound line 63