OAI/Geometry/PinnedDistances/MixtureLaw.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakPinned.Bounded.edgeWeight line 15
2. def OAI.WeakPinned.Bounded.tripleWeight line 17
3. lemma OAI.WeakPinned.Bounded.sum_edgeWeight line 20
4. lemma OAI.WeakPinned.Bounded.sum_tripleWeight line 24
5. def OAI.WeakPinned.Bounded.edgeValue line 28
6. def OAI.WeakPinned.Bounded.tripleValue line 31
7. lemma OAI.WeakPinned.Bounded.triple_integral line 34
8. lemma OAI.WeakPinned.Bounded.avg_abs_bound line 53
9. lemma OAI.WeakPinned.Bounded.pair_test_error line 62
10. lemma OAI.WeakPinned.Bounded.mixture_pair_test_bound line 69