OAI/Probability/LatticeSurface/Coercivity/SparseGradients.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SparseBlocks.volume_body_positive line 194
2. lemma OAI.SparseBlocks.volume_body_finite line 199
3. def OAI.SparseBlocks.law line 204
4. instance OAI.SparseBlocks.law_probability line 207
5. lemma OAI.SparseBlocks.law_real line 213
6. def OAI.SparseBlocks.window line 219
7. def OAI.SparseBlocks.edgeEvent line 221
8. def OAI.SparseBlocks.gradientEvent line 224
9. lemma OAI.SparseBlocks.closed_edgeEvent line 228
10. lemma OAI.SparseBlocks.closed_gradientEvent line 234
11. theorem OAI.SparseBlocks.joint_gradients line 239