OAI/Combinatorics/HalvingLines/Calculus.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PlanarHalving.Calculus.ae_near_set line 12
2. theorem OAI.PlanarHalving.Calculus.hasFDerivAt_of_within_near_set line 63
3. theorem OAI.PlanarHalving.Calculus.ae_differentiable_of_pointwise_lipschitz_pieces line 119
4. def OAI.PlanarHalving.Calculus.slopePiece line 137
5. theorem OAI.PlanarHalving.Calculus.measurableSet_slopePiece line 141
6. theorem OAI.PlanarHalving.Calculus.monotone_chord_bound line 151
7. theorem OAI.PlanarHalving.Calculus.slopePiece_bound line 167
8. theorem OAI.PlanarHalving.Calculus.mem_slopePiece_of_diagonal_differentiable line 181
9. theorem OAI.PlanarHalving.Calculus.bounded_monotone_ae_differentiable line 208
10. def OAI.PlanarHalving.Calculus.clampPoint line 235
11. lemma OAI.PlanarHalving.Calculus.clampPoint_mem line 238
12. lemma OAI.PlanarHalving.Calculus.clampPoint_eq line 244
13. lemma OAI.PlanarHalving.Calculus.clampPoint_monotone line 248
14. lemma OAI.PlanarHalving.Calculus.clampPoint_continuous line 253
15. theorem OAI.PlanarHalving.Calculus.bounded_monotoneOn_Icc_ae_differentiable line 257
16. theorem OAI.PlanarHalving.Calculus.bounded_monotoneOn_rectangle_ae_differentiable line 271
17. theorem OAI.PlanarHalving.Calculus.ae_differentiable_linear_change line 305