OAI/Computability/VertexCover/Analysis/PoincareOne.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.VertexCover.Cube.intervalLaw line 44
2. instance OAI.VertexCover.Cube.(instance at line 47) line 47
3. theorem OAI.VertexCover.Cube.integral_intervalLaw line 52
4. theorem OAI.VertexCover.Cube.intervalLaw_ac line 56
5. def OAI.VertexCover.Cube.law line 62
6. instance OAI.VertexCover.Cube.law_probability line 65
7. theorem OAI.VertexCover.Cube.sq_integral_le_measure_mul line 75
8. theorem OAI.VertexCover.Cube.deriv_memLp line 98
9. theorem OAI.VertexCover.Cube.anchored_sq_le line 103
10. theorem OAI.VertexCover.Cube.poincare_one line 137