OAI/Probability/LatticeSurface/Coercivity/ZeroPinnedSparse.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SparseBlocks.law_real_all line 281
2. lemma OAI.SparseBlocks.law_real_of_subset line 288
3. theorem OAI.SparseBlocks.zero_pinned_sparse line 292