Building blocks for the circle case

• mobiusFun c — the Möbius reparametrization x ↦ x / (x + c(1-x)) of the unit interval in ℝ≥0, packaged as an OpenPartialHomeomorph with its image lemmas: it lets us shrink the lower overlap component of a chart to sit below any ε > 0 while preserving the end-segment structure of images.
• affineNNRealOPH k d — the affine chart x ↦ k·x + d from Ioo 0 1 ⊆ ℝ≥0 onto Ioo d (d + k) ⊆ ℝ.
• Arithmetic for arcs in AddCircle 1: injectivity of the quotient map on short windows, period-shift identities, the frontier of a closed arc, and the covering of the circle by a closed arc and its complementary open arc.

noncomputable def OneMfld.mobiusFun (c x : NNReal) : NNReal

The Möbius reparametrization of the unit interval of ℝ≥0.

Equations

• OneMfld.mobiusFun c x = x / (x + c * (1 - x))

theorem OneMfld.exists_mobiusFun_lt {r ε : NNReal} (hr0 : 0 < r) (hr1 : r < 1) (hε : 0 < ε) : ∃ (c : NNReal), 0 < c ∧ mobiusFun c r < ε

mobiusFun c can push any interior point below any positive level, for large c.

theorem OneMfld.mobiusFun_strictMonoOn (c : NNReal) (hc : 0 < c) : StrictMonoOn (mobiusFun c) (Set.Ioo 0 1)

theorem OneMfld.mobiusFun_mem (c : NNReal) (hc : 0 < c) {t : NNReal} (ht : t ∈ Set.Ioo 0 1) : mobiusFun c t ∈ Set.Ioo 0 1

noncomputable def OneMfld.mobiusOPH' (c : NNReal) (hc : 0 < c) : { e : OpenPartialHomeomorph NNReal NNReal // e.source = Set.Ioo 0 1 ∧ e.target = Set.Ioo 0 1 ∧ (∀ (x : NNReal), ↑e.toPartialEquiv x = mobiusFun c x) ∧ (∀ t ∈ Set.Ioo 0 1, ↑e.toPartialEquiv '' Set.Ioo 0 t = Set.Ioo 0 (mobiusFun c t)) ∧ ∀ t ∈ Set.Ioo 0 1, ↑e.toPartialEquiv '' Set.Ioo t 1 = Set.Ioo (mobiusFun c t) 1 }

The Möbius reparametrization as a partial homeomorphism of Ioo 0 1 ⊆ ℝ≥0, with its action on lower and upper end-segments.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def OneMfld.affineNNRealOPH (k d : ℝ) (hk : 0 < k) : { e : OpenPartialHomeomorph NNReal ℝ // e.source = Set.Ioo 0 1 ∧ e.target = Set.Ioo d (d + k) ∧ ∀ (x : NNReal), ↑e.toPartialEquiv x = k * ↑x + d }

The affine map x ↦ k·x + d as a chart from Ioo 0 1 ⊆ ℝ≥0 onto Ioo d (d + k) ⊆ ℝ.

Equations

• One or more equations did not get rendered due to their size.

theorem OneMfld.addCircle_coe_inj {x y : ℝ} (h : ↑x = ↑y) (hxy : |x - y| < 1) : x = y

Two reals with the same image in AddCircle 1 and distance less than 1 are equal.

theorem OneMfld.addCircle_coe_add_one (x : ℝ) : ↑(x + 1) = ↑x

Shifting a real by the period 1 does not change its image in AddCircle 1.

theorem OneMfld.addCircle_arc_isClosed (c d : ℝ) : IsClosed (QuotientAddGroup.mk '' Set.Icc c d)

The closed arc coe '' Icc c d is closed in AddCircle 1.

theorem OneMfld.addCircle_arc_isOpen (c d : ℝ) : IsOpen (QuotientAddGroup.mk '' Set.Ioo c d)

The open arc coe '' Ioo c d is open in AddCircle 1.

theorem OneMfld.addCircle_frontier_arc_subset {c d : ℝ} : frontier (QuotientAddGroup.mk '' Set.Icc c d) ⊆ {↑c, ↑d}

The frontier of a closed arc is contained in its two endpoints.

theorem OneMfld.addCircle_arc_union_covers {c d : ℝ} (hcd : c ≤ d) (hlen : d < c + 1) : QuotientAddGroup.mk '' Set.Icc c d ∪ QuotientAddGroup.mk '' Set.Ioo d (c + 1) = Set.univ

A closed arc and the complementary open arc cover the circle.