OAI/Combinatorics/HalvingLines/Derivatives.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PlanarHalving.RankLimits.inv_cube_rpow line 11
  2. def OAI.PlanarHalving.RankLimits.goodPartition line 16
  3. lemma OAI.PlanarHalving.RankLimits.goodPartition_subset line 19
  4. lemma OAI.PlanarHalving.RankLimits.goodPartition_disjoint line 22
  5. lemma OAI.PlanarHalving.RankLimits.pow_depth line 27
  6. lemma OAI.PlanarHalving.RankLimits.Converges.goodPartition_loss line 30
  7. lemma OAI.PlanarHalving.RankLimits.Data.goodPartition_diagonal line 69
  8. lemma OAI.PlanarHalving.RankLimits.Data.goodPartition_crossings line 87
  9. lemma OAI.PlanarHalving.RankLimits.Converges.edge_crossing_null_closed line 116
  10. lemma OAI.PlanarHalving.RankLimits.Converges.edge_crossing_null line 153
  11. def OAI.PlanarHalving.RankLimits.CrossingPairs line 172
  12. instance OAI.PlanarHalving.RankLimits.crossingPairsCountable line 175
  13. lemma OAI.PlanarHalving.RankLimits.Converges.edge_crossing_ac line 179
  14. def OAI.PlanarHalving.RankLimit.extendRank line 202
  15. lemma OAI.PlanarHalving.RankLimit.extendRank_monotone line 205
  16. lemma OAI.PlanarHalving.RankLimit.extendRank_eq line 215
  17. theorem OAI.PlanarHalving.RankLimit.joint_tendsto_of_grid line 226
  18. theorem OAI.PlanarHalving.RankLimit.monotone_joint_subsequence line 265
  19. def OAI.PlanarHalving.RankLimits.signedPair line 287
  20. lemma OAI.PlanarHalving.RankLimits.continuous_signedPair line 290
  21. lemma OAI.PlanarHalving.RankLimits.signedPair_involutive line 295
  22. def OAI.PlanarHalving.RankLimits.pairCoordinates line 299
  23. lemma OAI.PlanarHalving.RankLimits.continuous_pairCoordinates line 302
  24. def OAI.PlanarHalving.RankLimits.Configuration.extendedRank line 307
  25. lemma OAI.PlanarHalving.RankLimits.Configuration.extendedRank_monotone line 311
  26. lemma OAI.PlanarHalving.RankLimits.Configuration.extendedRank_eq line 314
  27. lemma OAI.PlanarHalving.Limits.support_coordinate_identity line 354
  28. lemma OAI.PlanarHalving.RankLimits.Configuration.points_ae line 396
  29. lemma OAI.PlanarHalving.RankLimits.Converges.subseq line 403
  30. theorem OAI.PlanarHalving.RankLimits.Converges.rank_analytic line 409
  31. lemma OAI.PlanarHalving.Limits.positive_single_component line 448
  32. lemma OAI.PlanarHalving.Limits.restrict_ac_withDensity line 473