Building blocks for the H-H gluing

Two overlapping boundary charts glue to a closed interval, so the glued chart cannot be NNReal-valued (its target would not be open); it must land in the subtype UnitInterval. The pieces:

• halfOPH — x ↦ x/2 embedding Iio 1 ⊆ ℝ≥0 onto the lower half [0, 1/2) of the unit interval (open in the subtype since 0 is an endpoint);
• mobiusOPH k — the decreasing Möbius map x ↦ k/(x+k) embedding all of ℝ≥0 onto the upper piece (0, 1] (open in the subtype since 1 is an endpoint) — a decreasing reparametrization with no truncated-subtraction issues;
• the frontier of {y ≤ c} in the unit interval;
• reflection images of end-segments in ℝ≥0, used to re-orient OCharts.

noncomputable def OneMfld.halfOPH : { e : OpenPartialHomeomorph NNReal ↑UnitInterval // e.source = Set.Iio 1 ∧ e.target = {y : ↑UnitInterval | ↑y < 1 / 2} ∧ ∀ x ∈ Set.Iio 1, ↑(↑e x) = ↑x / 2 }

x ↦ x/2 as a partial homeomorphism from ℝ≥0 (source Iio 1) to the unit interval (target the sub-half-interval [0, 1/2), open in the subtype).

Equations

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

noncomputable def OneMfld.mobiusOPH (k : NNReal) (hk : 0 < k) : { e : OpenPartialHomeomorph NNReal ↑UnitInterval // e.source = Set.univ ∧ e.target = {y : ↑UnitInterval | 0 < ↑y} ∧ (∀ (x : NNReal), ↑(↑e x) = ↑k / (↑x + ↑k)) ∧ ∀ (x₁ x₂ : NNReal), x₁ < x₂ → ↑(↑e x₂) < ↑(↑e x₁) }

The Möbius map x ↦ k/(x+k) (for k > 0) as a partial homeomorphism from ℝ≥0 (source everything) to the unit interval (target (0, 1], open in the subtype). It is strictly decreasing, sends 0 ↦ 1, and tends to 0 at infinity.

Equations

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

theorem OneMfld.frontier_UIIic {c : ℝ} (h0 : 0 < c) (h1 : c < 1) : frontier {y : ↑UnitInterval | ↑y ≤ c} = {y : ↑UnitInterval | ↑y = c}

The frontier of the closed lower piece {y ≤ c} of the unit interval is the single level {y = c}, provided 0 < c < 1.

theorem OneMfld.reflect_image_Ioo_upper {p : NNReal} : (fun (y : NNReal) => 1 - y) '' Set.Ioo p 1 = Set.Ioo 0 (1 - p)

Reflection y ↦ 1 - y sends the upper end-segment Ioo p 1 ⊆ ℝ≥0 to the lower end-segment Ioo 0 (1-p).

theorem OneMfld.reflect_image_Ioo_lower {q : NNReal} (hq1 : q ≤ 1) : (fun (y : NNReal) => 1 - y) '' Set.Ioo 0 q = Set.Ioo (1 - q) 1

Reflection y ↦ 1 - y sends the lower end-segment Ioo 0 q ⊆ ℝ≥0 (for q ≤ 1) to the upper end-segment Ioo (1-q) 1.