OAI/Combinatorics/SparsestCut/InterfaceStep.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.UniformSparsestCut.InterfaceStep.telescoping_events line 15
2. lemma OAI.UniformSparsestCut.InterfaceStep.threshold_decomposition line 58
3. lemma OAI.UniformSparsestCut.InterfaceStep.integral_deriv_eq_zero line 87
4. lemma OAI.UniformSparsestCut.InterfaceStep.threshold_integral_deriv line 94
5. lemma OAI.UniformSparsestCut.InterfaceStep.measurable_filter_apply line 128
6. lemma OAI.UniformSparsestCut.InterfaceStep.eventually_threshold_eq line 148
7. lemma OAI.UniformSparsestCut.InterfaceStep.continuousAt_threshold_integral line 162
8. lemma OAI.UniformSparsestCut.InterfaceStep.threshold_integral line 185
9. lemma OAI.UniformSparsestCut.InterfaceStep.tail_integral_hasDerivAt line 211
10. lemma OAI.UniformSparsestCut.InterfaceStep.eventually_order_eq line 224
11. lemma OAI.UniformSparsestCut.InterfaceStep.moving_threshold_integral_hasDerivAt line 265
12. lemma OAI.UniformSparsestCut.InterfaceStep.integral_deriv_zero_off_countable line 294
13. lemma OAI.UniformSparsestCut.InterfaceStep.affine_collisions_countable line 321
14. lemma OAI.UniformSparsestCut.InterfaceStep.moving_threshold_weak line 341
15. lemma OAI.UniformSparsestCut.InterfaceStep.threshold_integrable line 377
16. lemma OAI.UniformSparsestCut.InterfaceStep.threshold_pointwise_bound line 388
17. lemma OAI.UniformSparsestCut.InterfaceStep.threshold_integral_diff_bound line 417
18. lemma OAI.UniformSparsestCut.InterfaceStep.moving_threshold_integral_hasFDerivAt line 457
19. lemma OAI.UniformSparsestCut.InterfaceStep.affine_threshold_lipschitz line 482
20. lemma OAI.UniformSparsestCut.InterfaceStep.averaged_threshold_derivative line 511