Weighted subdivisions of the circle

A positive list of integral weights determines the orientation-preserving piecewise-linear map which sends the ith unit interval to an interval of length equal to the ith weight. This file packages that map as a homeomorphism of intervals and, after identifying endpoints, as a homeomorphism of circles. It is the geometric core of Gallier--Xu P1 edge subdivision.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.WeightedCircle.stretch : List ℕ → ℝ → ℝ

Piecewise-linear cumulative stretching by a list of integral weights.

Equations

• One or more equations did not get rendered due to their size.
• LeanEval.Topology.ClassificationOfSurfaces.WeightedCircle.stretch [] x✝ = 0

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.WeightedCircle.unstretch : List ℕ → ℝ → ℝ

The inverse piecewise-linear cumulative stretching.

Equations

• One or more equations did not get rendered due to their size.
• LeanEval.Topology.ClassificationOfSurfaces.WeightedCircle.unstretch [] x✝ = 0

def LeanEval.Topology.ClassificationOfSurfaces.WeightedCircle.Positive (weights : List ℕ) : Prop

Every weight is strictly positive.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.WeightedCircle.Positive weights = ∀ w ∈ weights, 0 < w

theorem LeanEval.Topology.ClassificationOfSurfaces.WeightedCircle.Positive.head {w : ℕ} {weights : List ℕ} (h : Positive (w :: weights)) : 0 < w

theorem LeanEval.Topology.ClassificationOfSurfaces.WeightedCircle.Positive.tail {w : ℕ} {weights : List ℕ} (h : Positive (w :: weights)) : Positive weights

theorem LeanEval.Topology.ClassificationOfSurfaces.WeightedCircle.sum_take_lt_sum {weights : List ℕ} (h : Positive weights) (i : Fin weights.length) : (List.take (↑i) weights).sum < weights.sum

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.WeightedCircle.stretch_nil (x : ℝ) : stretch [] x = 0

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.WeightedCircle.unstretch_nil (y : ℝ) : unstretch [] y = 0

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.WeightedCircle.stretch_zero (weights : List ℕ) : stretch weights 0 = 0

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.WeightedCircle.unstretch_zero (weights : List ℕ) : unstretch weights 0 = 0

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.WeightedCircle.stretch_length (weights : List ℕ) : stretch weights ↑weights.length = ↑weights.sum

theorem LeanEval.Topology.ClassificationOfSurfaces.WeightedCircle.unstretch_sum (weights : List ℕ) (h : Positive weights) : unstretch weights ↑weights.sum = ↑weights.length

theorem LeanEval.Topology.ClassificationOfSurfaces.WeightedCircle.continuous_stretch (weights : List ℕ) : Continuous (stretch weights)

Stretching is continuous; adjacent affine pieces agree at every breakpoint.

theorem LeanEval.Topology.ClassificationOfSurfaces.WeightedCircle.continuous_unstretch (weights : List ℕ) (h : Positive weights) : Continuous (unstretch weights)

Inverse stretching is continuous when every weight is positive.

theorem LeanEval.Topology.ClassificationOfSurfaces.WeightedCircle.stretch_nonneg {weights : List ℕ} (h : Positive weights) {x : ℝ} (hx0 : 0 ≤ x) (hxlen : x ≤ ↑weights.length) : 0 ≤ stretch weights x

theorem LeanEval.Topology.ClassificationOfSurfaces.WeightedCircle.stretch_le_sum {weights : List ℕ} (h : Positive weights) {x : ℝ} (hx0 : 0 ≤ x) (hxlen : x ≤ ↑weights.length) : stretch weights x ≤ ↑weights.sum

theorem LeanEval.Topology.ClassificationOfSurfaces.WeightedCircle.stretch_pos {weights : List ℕ} (h : Positive weights) {x : ℝ} (hx0 : 0 < x) (hxlen : x ≤ ↑weights.length) : 0 < stretch weights x

theorem LeanEval.Topology.ClassificationOfSurfaces.WeightedCircle.unstretch_nonneg {weights : List ℕ} (h : Positive weights) {y : ℝ} (hy0 : 0 ≤ y) (hysum : y ≤ ↑weights.sum) : 0 ≤ unstretch weights y

theorem LeanEval.Topology.ClassificationOfSurfaces.WeightedCircle.unstretch_le_length {weights : List ℕ} (h : Positive weights) {y : ℝ} (hy0 : 0 ≤ y) (hysum : y ≤ ↑weights.sum) : unstretch weights y ≤ ↑weights.length

theorem LeanEval.Topology.ClassificationOfSurfaces.WeightedCircle.unstretch_pos {weights : List ℕ} (h : Positive weights) {y : ℝ} (hy0 : 0 < y) (hysum : y ≤ ↑weights.sum) : 0 < unstretch weights y

theorem LeanEval.Topology.ClassificationOfSurfaces.WeightedCircle.unstretch_stretch {weights : List ℕ} (h : Positive weights) {x : ℝ} (hx0 : 0 ≤ x) (hxlen : x ≤ ↑weights.length) : unstretch weights (stretch weights x) = x

theorem LeanEval.Topology.ClassificationOfSurfaces.WeightedCircle.stretch_unstretch {weights : List ℕ} (h : Positive weights) {y : ℝ} (hy0 : 0 ≤ y) (hysum : y ≤ ↑weights.sum) : stretch weights (unstretch weights y) = y

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.WeightedCircle.intervalHomeomorph (weights : List ℕ) (h : Positive weights) : ↑(Set.Icc 0 (0 + ↑weights.length)) ≃ₜ ↑(Set.Icc 0 (0 + ↑weights.sum))

Positive weights give a homeomorphism from the interval of positions to the interval of expanded positions.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.WeightedCircle.intervalHomeomorph_apply_val (weights : List ℕ) (h : Positive weights) (x : ↑(Set.Icc 0 (0 + ↑weights.length))) : ↑((intervalHomeomorph weights h) x) = stretch weights ↑x

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.WeightedCircle.intervalHomeomorph_zero (weights : List ℕ) (h : Positive weights) : (intervalHomeomorph weights h) ⟨0, ⋯⟩ = ⟨0, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.WeightedCircle.intervalHomeomorph_length (weights : List ℕ) (h : Positive weights) : (intervalHomeomorph weights h) ⟨0 + ↑weights.length, ⋯⟩ = ⟨0 + ↑weights.sum, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.WeightedCircle.intervalHomeomorph_endpointIdent_iff (weights : List ℕ) (h : Positive weights) [Fact (0 < ↑weights.length)] [Fact (0 < ↑weights.sum)] (x y : ↑(Set.Icc 0 (0 + ↑weights.length))) : AddCircle.EndpointIdent (↑weights.length) 0 x y ↔ AddCircle.EndpointIdent (↑weights.sum) 0 ((intervalHomeomorph weights h) x) ((intervalHomeomorph weights h) y)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.WeightedCircle.endpointQuotHomeomorph (weights : List ℕ) (h : Positive weights) [Fact (0 < ↑weights.length)] [Fact (0 < ↑weights.sum)] : Quot (AddCircle.EndpointIdent (↑weights.length) 0) ≃ₜ Quot (AddCircle.EndpointIdent (↑weights.sum) 0)

The interval homeomorphism descends after identifying both pairs of endpoints.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.WeightedCircle.addCircleHomeomorph (weights : List ℕ) (h : Positive weights) (hne : weights ≠ []) : AddCircle ↑weights.length ≃ₜ AddCircle ↑weights.sum

The weighted interval map with endpoints identified, as a homeomorphism of additive circles.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.WeightedCircle.circleHomeomorph (weights : List ℕ) (h : Positive weights) (hne : weights ≠ []) : Circle ≃ₜ Circle

The weighted subdivision homeomorphism transported to the complex unit circle.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.WeightedCircle.addCircleHomeomorph_apply_of_mem_Ico (weights : List ℕ) (h : Positive weights) (hne : weights ≠ []) (x : ℝ) (hx : x ∈ Set.Ico 0 ↑weights.length) : (addCircleHomeomorph weights h hne) ↑x = ↑(stretch weights x)

theorem LeanEval.Topology.ClassificationOfSurfaces.WeightedCircle.circleHomeomorph_exp_of_mem_Ico (weights : List ℕ) (h : Positive weights) (hne : weights ≠ []) (x : ℝ) (hx : x ∈ Set.Ico 0 ↑weights.length) : (circleHomeomorph weights h hne) (Circle.exp (2 * Real.pi / ↑weights.length * x)) = Circle.exp (2 * Real.pi / ↑weights.sum * stretch weights x)

On the fundamental interval, the circle homeomorphism is exactly the weighted piecewise-linear angular map.

theorem LeanEval.Topology.ClassificationOfSurfaces.WeightedCircle.stretch_index_add (weights : List ℕ) (i : Fin weights.length) (t : ↑unitInterval) : stretch weights (↑↑i + ↑t) = ↑(List.take (↑i) weights).sum + ↑(weights.get i) * ↑t

On the ith unit interval, stretching is affine with slope equal to the ith weight.

theorem LeanEval.Topology.ClassificationOfSurfaces.WeightedCircle.circleHomeomorph_exp_index_add (weights : List ℕ) (h : Positive weights) (hne : weights ≠ []) (i : Fin weights.length) (t : ↑unitInterval) (hnotLastEndpoint : ↑↑i + ↑t < ↑weights.length) : (circleHomeomorph weights h hne) (Circle.exp (2 * Real.pi / ↑weights.length * (↑↑i + ↑t))) = Circle.exp (2 * Real.pi / ↑weights.sum * (↑(List.take (↑i) weights).sum + ↑(weights.get i) * ↑t))

The weighted circle homeomorphism sends a point of side i to the boundary coordinate obtained by adding the weighted prefix and the affine local parameter.

theorem LeanEval.Topology.ClassificationOfSurfaces.WeightedCircle.circleHomeomorph_exp_index_add' (weights : List ℕ) (h : Positive weights) (hne : weights ≠ []) (i : Fin weights.length) (t : ↑unitInterval) : (circleHomeomorph weights h hne) (Circle.exp (2 * Real.pi / ↑weights.length * (↑↑i + ↑t))) = Circle.exp (2 * Real.pi / ↑weights.sum * (↑(List.take (↑i) weights).sum + ↑(weights.get i) * ↑t))

Endpoint-inclusive form of circleHomeomorph_exp_index_add. The only additional case is the terminal endpoint of the last source interval; both displayed angles then represent the basepoint of their respective circles.