OAI/Combinatorics/HalvingLines/Continuity.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarHalving.TimeWindows.lower line 11
  2. def OAI.PlanarHalving.TimeWindows.upper line 12
  3. lemma OAI.PlanarHalving.TimeWindows.lower_lt_upper line 14
  4. lemma OAI.PlanarHalving.TimeWindows.upper_sub_lower line 19
  5. lemma OAI.PlanarHalving.TimeWindows.Ioo_subset_carrier line 24
  6. lemma OAI.PlanarHalving.TimeWindows.carrier_subset_Icc line 31
  7. lemma OAI.PlanarHalving.TimeWindows.closure_carrier line 38
  8. lemma OAI.PlanarHalving.TimeWindows.endpoints_of_subset line 44
  9. lemma OAI.PlanarHalving.TimeWindows.before_or_before line 51
  10. lemma OAI.PlanarHalving.TimeWindows.before_of_separated line 64
  11. lemma OAI.PlanarHalving.TimeWindows.ae_avoid_boundaries line 68
  12. lemma OAI.PlanarHalving.TimeWindows.exists_separated_positive line 76
  13. lemma OAI.PlanarHalving.Batches.System.windowCrossings_comm line 141
  14. lemma OAI.PlanarHalving.Batches.System.windowCrossMeasure_comm line 150
  15. lemma OAI.PlanarHalving.RankLimits.Converges.crossings_comm line 164
  16. lemma OAI.PlanarHalving.RankLimits.unitPair_quasiMeasurePreserving line 171
  17. lemma OAI.PlanarHalving.RankLimits.signedPair_measurePreserving line 177
  18. lemma OAI.PlanarHalving.RankLimits.Converges.crossing_real_projection line 182
  19. lemma OAI.PlanarHalving.RankLimits.Converges.crossing_signed_projection line 193
  20. lemma OAI.PlanarHalving.RankLimits.Converges.window_withDensity line 203
  21. lemma OAI.PlanarHalving.RankLimits.Converges.edge_probability line 214
  22. lemma OAI.PlanarHalving.RankLimit.dense_strict_brackets line 227
  23. lemma OAI.PlanarHalving.RankLimit.monotone_eventually_uniform_approx line 249
  24. lemma OAI.PlanarHalving.RankLimit.firstOrder_eventually_uniform line 290
  25. lemma OAI.PlanarHalving.RankLimit.firstOrder_of_joint line 330
  26. def OAI.PlanarHalving.RankLimits.SeparatedBefore line 352
  27. lemma OAI.PlanarHalving.RankLimits.Data.exists_positive_windows line 355
  28. theorem OAI.PlanarHalving.RankLimits.Converges.positive_part line 379