OAI/Analysis/TriangularHilbert/CyclicNorm.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TriangularHilbert.mainConstant line 11
2. lemma OAI.TriangularHilbert.coe_mainConstant line 13
3. lemma OAI.TriangularHilbert.ofReal_integral_cube line 17
4. lemma OAI.TriangularHilbert.integral_cube_eq_one line 24
5. lemma OAI.TriangularHilbert.cyclicNorm_le_unit line 30
6. lemma OAI.TriangularHilbert.cyclicNorm_le line 39