OAI/Analysis/CircleDomains/Topology/CircleQuantileArcs.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Four positively separated arcs from a fixed countable circle family.

  1. def OAI.CircleDomainRigidity.unitCircleCut line 15
  2. theorem OAI.CircleDomainRigidity.unitCircleCut_mem line 17
  3. theorem OAI.CircleDomainRigidity.unitCircleCut_injective line 20
  4. theorem OAI.CircleDomainRigidity.continuousAt_unitCircleCut line 24
  5. theorem OAI.CircleDomainRigidity.measurable_unitCircleCut line 28
  6. def OAI.CircleDomainRigidity.rationalCircleArc line 33
  7. theorem OAI.CircleDomainRigidity.measurableSet_rationalCircleArc line 36
  8. theorem OAI.CircleDomainRigidity.isOpen_rationalCircleArc line 39
  9. theorem OAI.CircleDomainRigidity.nullSingletonClass_unitCircleCut_map line 54
  10. theorem OAI.CircleDomainRigidity.unitCircleCut_cdf_endpoints line 65
  11. theorem OAI.CircleDomainRigidity.exists_four_ordered_rational_circle_arcs line 91

    Source documentation

    All four arcs can be taken from the countable rational endpoint family, with cyclic order witnessed inside a single cut of the circle.

    theorem exists_four_ordered_rational_circle_arcs (μ : ProbabilityMeasure UnitAddCircle)
    [NullSingletonClass (μ : Measure UnitAddCircle)] :
    ∃ l u : Fin 4 → ℚ,
      (∀ i, 0 < l i ∧ l i < u i ∧ u i < 1 ∧
        (1 / 10 : ℝ≥0∞) < (μ : Measure UnitAddCircle) (rationalCircleArc (l i) (u i))) ∧
      ∀ i j, i < j → u i < l j := by
…

    Mentions: OAI.CircleDomainRigidity.rationalCircleArc