OAI/Analysis/TriangularHilbert/StrongLayer.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TriangularHilbert.squareLayer line 11
2. def OAI.TriangularHilbert.oneLayer line 13
3. lemma OAI.TriangularHilbert.squareLayer_integrable line 15
4. lemma OAI.TriangularHilbert.oneLayer_integrable line 20
5. lemma OAI.TriangularHilbert.integral_squareLayer line 25
6. lemma OAI.TriangularHilbert.integral_oneLayer line 35
7. lemma OAI.TriangularHilbert.layer_iff line 41