OAI/Geometry/PinnedDistances/FiniteMixtures.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakPinned.Bounded.finiteLaw_fst line 16
2. lemma OAI.WeakPinned.Bounded.tripleLaw_edge line 27
3. lemma OAI.WeakPinned.Bounded.finiteLaw_mono line 45
4. lemma OAI.WeakPinned.Bounded.finiteLaw_prod line 55
5. lemma OAI.WeakPinned.Bounded.finiteLaw_smul line 63
6. lemma OAI.WeakPinned.Bounded.graph_edge_eval line 82
7. lemma OAI.WeakPinned.Bounded.graph_edge_law line 89
8. lemma OAI.WeakPinned.Bounded.pairProb_le_uniform line 109
9. lemma OAI.WeakPinned.Bounded.graph_domination line 121