OAI/Combinatorics/SparsestCut/Profiles.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniformSparsestCut.Profile.pairing line 16
2. def OAI.UniformSparsestCut.Profile.differential line 21
3. lemma OAI.UniformSparsestCut.Profile.pairing_hasDeriv line 28
4. lemma OAI.UniformSparsestCut.Profile.differential_correction line 52
5. lemma OAI.UniformSparsestCut.Profile.cancellation line 94
6. lemma OAI.UniformSparsestCut.Profile.active_cancellation line 129
7. lemma OAI.UniformSparsestCut.Profile.active_bound line 161
8. def OAI.UniformSparsestCut.Profile.kernel line 208
9. lemma OAI.UniformSparsestCut.Profile.pairing_continuousOn line 211
10. lemma OAI.UniformSparsestCut.Profile.pairing_integrable line 225
11. lemma OAI.UniformSparsestCut.Profile.pairing_correction line 232
12. lemma OAI.UniformSparsestCut.Profile.kernel_correction line 257
13. lemma OAI.UniformSparsestCut.Profile.integral_inv_sq line 291
14. lemma OAI.UniformSparsestCut.Profile.kernel_segment_bound line 304