OAI/Probability/LatticeSurface/Coercivity/MomentBuffer.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SparseHoles.square_eq_box line 35
2. lemma OAI.SparseHoles.square_card line 37
3. lemma OAI.SparseHoles.buffer_card line 42
4. lemma OAI.SparseHoles.square_card_bound line 47
5. lemma OAI.SparseHoles.buffer_edges_bound line 52
6. lemma OAI.SparseHoles.moment_buffer line 60
7. lemma OAI.SparseHoles.square_lipschitz line 77
8. lemma OAI.SparseHoles.bounded_square_test line 90