OAI/Analysis/TriangularHilbert/BoundedBox.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TriangularHilbert.closedBox line 13
2. lemma OAI.TriangularHilbert.mem_closedBox line 14
3. lemma OAI.TriangularHilbert.measurableSet_closedBox line 16
4. lemma OAI.TriangularHilbert.isCompact_closedBox line 17
5. lemma OAI.TriangularHilbert.volume_closedBox_ne_top line 18
6. def OAI.TriangularHilbert.BoxSupport line 20
7. lemma OAI.TriangularHilbert.compactSupport_box line 23
8. lemma OAI.TriangularHilbert.sampled_cubic_tendsto line 32