OAI/Combinatorics/HalvingLines/PathLimits.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PlanarHalving.Batches.ConvexPath.extension_vertex line 11
2. lemma OAI.PlanarHalving.Batches.ConvexPath.extension_left line 28
3. lemma OAI.PlanarHalving.Batches.ConvexPath.extension_right line 47
4. lemma OAI.PlanarHalving.Batches.finite_intermediate line 66
5. lemma OAI.PlanarHalving.Batches.ConvexPath.extension_middle line 80
6. lemma OAI.PlanarHalving.Batches.ConvexPath.extension_cases line 106
7. theorem OAI.PlanarHalving.Spatial.subsequence_of_asymptotic_continuity line 126
8. lemma OAI.PlanarHalving.Spatial.asymptotic_continuity_of_radial line 177
9. lemma OAI.PlanarHalving.Spatial.lower_distance_of_limit line 191
10. lemma OAI.PlanarHalving.Spatial.geometric_scale line 204
11. lemma OAI.PlanarHalving.Spatial.geometric_lower_power line 227
12. lemma OAI.PlanarHalving.Spatial.inverse_holder_of_radial_limits line 243
13. theorem OAI.PlanarHalving.Limits.finiteMeasure_subsequence line 269
14. lemma OAI.PlanarHalving.RankCoordinates.variation_le_two line 295
15. lemma OAI.PlanarHalving.RankCoordinates.min_le_of_quasiconcave line 331
16. lemma OAI.PlanarHalving.RankCoordinates.concave_cdf_variation line 344
17. lemma OAI.PlanarHalving.RankCoordinates.sigmoid_variation line 353
18. lemma OAI.PlanarHalving.RankCoordinates.smoothed_variation line 361