Transporting the elementary move to a thin kite

The fixed diamond used to prove the barycentric fan move is too large for the relative Schoenflies induction. This file transports it piecewise-affinely to a kite whose lower and upper margins are an arbitrary positive δ. The two halves of the outer kite form a two-triangle mesh, so the transport is supplied by the canonical realization homeomorphism.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.axisKitePosition (lo hi : ℝ) : Fin 4 → Plane

Left, right, top, and bottom vertices of an axis-aligned kite.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.axisKitePosition_zero (lo hi : ℝ) : axisKitePosition lo hi 0 = planePoint (-1) 0

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.axisKitePosition_one (lo hi : ℝ) : axisKitePosition lo hi 1 = planePoint 1 0

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.axisKitePosition_two (lo hi : ℝ) : axisKitePosition lo hi 2 = planePoint 0 hi

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.axisKitePosition_three (lo hi : ℝ) : axisKitePosition lo hi 3 = planePoint 0 lo

def LeanEval.Topology.ClassificationOfSurfaces.Moise.axisKiteTriangles : Finset (Finset (Fin 4))

The axisKiteTriangles declaration.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.axisKiteTriangles = {{0, 2, 3}, {1, 2, 3}}

def LeanEval.Topology.ClassificationOfSurfaces.Moise.axisKitePatch (lo hi : ℝ) : Set Plane

The axisKitePatch declaration.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.axisKitePosition_injective {lo hi : ℝ} (hlo : lo < 0) (hhi : 0 < hi) : Function.Injective (axisKitePosition lo hi)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.axisKite_affineIndependent {lo hi : ℝ} (hlo : lo < 0) (hhi : 0 < hi) {t : Finset (Fin 4)} (ht : t ∈ axisKiteTriangles) : AffineIndependent ℝ fun (v : ↥t) => axisKitePosition lo hi ↑v

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.axisKite_inter {lo hi : ℝ} (hlo : lo < 0) (hhi : 0 < hi) : (convexHull ℝ) (axisKitePosition lo hi '' ↑{0, 2, 3}) ∩ (convexHull ℝ) (axisKitePosition lo hi '' ↑{1, 2, 3}) = (convexHull ℝ) (axisKitePosition lo hi '' ↑({0, 2, 3} ∩ {1, 2, 3}))

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.axisKiteMesh (lo hi : ℝ) (hlo : lo < 0) (hhi : 0 < hi) : TriangleMesh

The axisKiteMesh declaration.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.axisKiteMesh_support (lo hi : ℝ) (hlo : lo < 0) (hhi : 0 < hi) : (axisKiteMesh lo hi hlo hhi).toPlaneComplex.support = axisKitePatch lo hi

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.axisKitePatch_negTwo_two : axisKitePatch (-2) 2 = diamondPatch

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.thinKiteScale (δ : ℝ) : ℝ

Vertical scale used to compress the fixed diamond to a kite with margins δ.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.thinKiteScale δ = (1 + 2 * δ) / 4

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.thinKiteMap (δ : ℝ) (p : Plane) : Plane

The global piecewise-affine transport. Writing the two affine pieces with |x| makes continuity across the vertical diagonal immediate.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.thinKiteInv (δ : ℝ) (p : Plane) : Plane

The thinKiteInv declaration.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.thinKiteScale_pos {δ : ℝ} (hδ : 0 < δ) : 0 < thinKiteScale δ

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.thinKiteGlobalHomeomorph (δ : ℝ) (hδ : 0 < δ) : Plane ≃ₜ Plane

The thinKiteGlobalHomeomorph declaration.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.thinKitePatch (δ : ℝ) : Set Plane

The thin kite is the image of the fixed diamond under the explicit transport.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.thinKitePatch_subset_leftCone {δ : ℝ} (hδ : 0 ≤ δ) {p : Plane} (hp : p ∈ thinKitePatch δ) : 0 ≤ p.ofLp 0 + 1 ∧ -δ * (p.ofLp 0 + 1) ≤ p.ofLp 1 ∧ p.ofLp 1 ≤ (1 + δ) * (p.ofLp 0 + 1)

Every point of the thin kite lies in the tangent cone at its left base vertex.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.thinKitePatch_subset_rightCone {δ : ℝ} (hδ : 0 ≤ δ) {p : Plane} (hp : p ∈ thinKitePatch δ) : 0 ≤ 1 - p.ofLp 0 ∧ -δ * (1 - p.ofLp 0) ≤ p.ofLp 1 ∧ p.ofLp 1 ≤ (1 + δ) * (1 - p.ofLp 0)

Every point of the thin kite lies in the tangent cone at its right base vertex.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.kiteTrianglePosition : Fin 3 → Plane

The triangle onto which the thin kite collapses when δ = 0.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.kiteTrianglePosition_affineIndependent : AffineIndependent ℝ kiteTrianglePosition

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.exists_leftBase_openSegment_mem_kiteTriangle {q : Plane} (hq : q ≠ planePoint (-1) 0) (hx : 0 < q.ofLp 0 + 1) (hy0 : 0 ≤ q.ofLp 1) (hyx : q.ofLp 1 ≤ q.ofLp 0 + 1) : ∃ p ∈ segment ℝ (planePoint (-1) 0) q \ {planePoint (-1) 0}, p ∈ (convexHull ℝ) (Set.range kiteTrianglePosition)

A ray from the left base vertex whose coordinate direction lies in the original triangle cone enters the triangle immediately.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.exists_rightBase_openSegment_mem_kiteTriangle {q : Plane} (hq : q ≠ planePoint 1 0) (hx : 0 < 1 - q.ofLp 0) (hy0 : 0 ≤ q.ofLp 1) (hyx : q.ofLp 1 ≤ 1 - q.ofLp 0) : ∃ p ∈ segment ℝ (planePoint 1 0) q \ {planePoint 1 0}, p ∈ (convexHull ℝ) (Set.range kiteTrianglePosition)

A ray from the right base vertex whose direction lies in the original triangle cone enters the triangle immediately.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.leftBase_direction_outside_kiteTriangle {q : Plane} (hq : q ≠ planePoint (-1) 0) (havoid : segment ℝ (planePoint (-1) 0) q ∩ (convexHull ℝ) (Set.range kiteTrianglePosition) ⊆ {planePoint (-1) 0}) : q.ofLp 0 + 1 ≤ 0 ∨ 0 < q.ofLp 0 + 1 ∧ (q.ofLp 1 < 0 ∨ q.ofLp 0 + 1 < q.ofLp 1)

If a segment leaves the left base vertex without entering the triangle, its direction is strictly outside the triangle tangent cone.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.rightBase_direction_outside_kiteTriangle {q : Plane} (hq : q ≠ planePoint 1 0) (havoid : segment ℝ (planePoint 1 0) q ∩ (convexHull ℝ) (Set.range kiteTrianglePosition) ⊆ {planePoint 1 0}) : 1 - q.ofLp 0 ≤ 0 ∨ 0 < 1 - q.ofLp 0 ∧ (q.ofLp 1 < 0 ∨ 1 - q.ofLp 0 < q.ofLp 1)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.exists_thinKitePatch_inter_leftSegment_eq_singleton {q : Plane} (hq : q ≠ planePoint (-1) 0) (havoid : segment ℝ (planePoint (-1) 0) q ∩ (convexHull ℝ) (Set.range kiteTrianglePosition) ⊆ {planePoint (-1) 0}) : ∃ (ε : ℝ), 0 < ε ∧ ∀ (δ : ℝ), 0 < δ → δ < ε → thinKitePatch δ ∩ segment ℝ (planePoint (-1) 0) q = {planePoint (-1) 0}

A segment leaving the left base vertex outside the triangle misses every sufficiently thin kite except at that vertex.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.exists_thinKitePatch_inter_rightSegment_eq_singleton {q : Plane} (hq : q ≠ planePoint 1 0) (havoid : segment ℝ (planePoint 1 0) q ∩ (convexHull ℝ) (Set.range kiteTrianglePosition) ⊆ {planePoint 1 0}) : ∃ (ε : ℝ), 0 < ε ∧ ∀ (δ : ℝ), 0 < δ → δ < ε → thinKitePatch δ ∩ segment ℝ (planePoint 1 0) q = {planePoint 1 0}

A segment leaving the right base vertex outside the triangle misses every sufficiently thin kite except at that vertex.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.thinKiteMap_zero_mem_triangle {q : Plane} (hq : q ∈ diamondPatch) : thinKiteMap 0 q ∈ (convexHull ℝ) (Set.range kiteTrianglePosition)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.exists_thinKitePatch_subset_open_normalized (U : Set Plane) (hU : IsOpen U) (htriangle : (convexHull ℝ) (Set.range kiteTrianglePosition) ⊆ U) : ∃ (ε : ℝ), 0 < ε ∧ ∀ (δ : ℝ), 0 < δ → δ < ε → thinKitePatch δ ⊆ U

Every open neighborhood of the limiting triangle contains all sufficiently thin normalized kites.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.exists_thinKitePatch_inter_segment_subset_baseEndpoints {a b : Plane} (hab : a ≠ b) (hinter : segment ℝ a b ∩ (convexHull ℝ) (Set.range kiteTrianglePosition) ⊆ {planePoint (-1) 0, planePoint 1 0}) (hleftEndpoint : planePoint (-1) 0 ∈ segment ℝ a b → a = planePoint (-1) 0 ∨ b = planePoint (-1) 0) (hrightEndpoint : planePoint 1 0 ∈ segment ℝ a b → a = planePoint 1 0 ∨ b = planePoint 1 0) (hnotBoth : ¬(planePoint (-1) 0 ∈ segment ℝ a b ∧ planePoint 1 0 ∈ segment ℝ a b)) : ∃ (ε : ℝ), 0 < ε ∧ ∀ (δ : ℝ), 0 < δ → δ < ε → thinKitePatch δ ∩ segment ℝ a b ⊆ {planePoint (-1) 0, planePoint 1 0}

A finite-mesh edge which meets the limiting triangle in at most one base endpoint is avoided by every sufficiently thin kite, apart from that endpoint.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondOuterToThinKite (δ : ℝ) (hδ : 0 < δ) : ↑diamondPatch ≃ₜ ↑(thinKitePatch δ)

The diamondOuterToThinKite declaration.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.thinKiteSource (δ : ℝ) : ℝ

The thinKiteSource declaration.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.thinKiteSource δ = -2 / (1 + 2 * δ)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.thinKiteTarget (δ : ℝ) : ℝ

The thinKiteTarget declaration.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.thinKiteTarget δ = 2 / (1 + 2 * δ)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.thinKiteSource_lower {δ : ℝ} (hδ : 0 < δ) : -2 < thinKiteSource δ

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.thinKiteSource_upper {δ : ℝ} (hδ : 0 < δ) : thinKiteSource δ < 2

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.thinKiteTarget_lower {δ : ℝ} (hδ : 0 < δ) : -2 < thinKiteTarget δ

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.thinKiteTarget_upper {δ : ℝ} (hδ : 0 < δ) : thinKiteTarget δ < 2

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.thinKiteMap_source (δ : ℝ) (hδ : 0 < δ) : thinKiteMap δ (planePoint 0 (thinKiteSource δ)) = planePoint 0 0

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.thinKiteMap_target (δ : ℝ) (hδ : 0 < δ) : thinKiteMap δ (planePoint 0 (thinKiteTarget δ)) = planePoint 0 1

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.isClosed_thinKitePatch (δ : ℝ) : IsClosed (thinKitePatch δ)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.thinKiteAmbientHomeomorph (δ : ℝ) (hδ : 0 < δ) : Plane ≃ₜ Plane

The thinKiteAmbientHomeomorph declaration.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.thinKiteAmbientHomeomorph_leftSpoke (δ : ℝ) (hδ : 0 < δ) (c : ℝ) (hc : c ∈ Set.Icc 0 1) : (thinKiteAmbientHomeomorph δ hδ) ((AffineMap.lineMap (planePoint (-1) 0) (planePoint 0 0)) c) = (AffineMap.lineMap (planePoint (-1) 0) (planePoint 0 1)) c

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.thinKiteAmbientHomeomorph_rightSpoke (δ : ℝ) (hδ : 0 < δ) (c : ℝ) (hc : c ∈ Set.Icc 0 1) : (thinKiteAmbientHomeomorph δ hδ) ((AffineMap.lineMap (planePoint 1 0) (planePoint 0 0)) c) = (AffineMap.lineMap (planePoint 1 0) (planePoint 0 1)) c

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.thinKiteAmbientHomeomorph_image_leftSpoke (δ : ℝ) (hδ : 0 < δ) : ⇑(thinKiteAmbientHomeomorph δ hδ) '' segment ℝ (planePoint (-1) 0) (planePoint 0 0) = segment ℝ (planePoint (-1) 0) (planePoint 0 1)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.thinKiteAmbientHomeomorph_image_rightSpoke (δ : ℝ) (hδ : 0 < δ) : ⇑(thinKiteAmbientHomeomorph δ hδ) '' segment ℝ (planePoint 1 0) (planePoint 0 0) = segment ℝ (planePoint 1 0) (planePoint 0 1)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.thinKiteAmbientHomeomorph_image_segment_of_endpoints_mem_leftSpoke (δ : ℝ) (hδ : 0 < δ) {a b : Plane} (ha : a ∈ segment ℝ (planePoint (-1) 0) (planePoint 0 0)) (hb : b ∈ segment ℝ (planePoint (-1) 0) (planePoint 0 0)) : ⇑(thinKiteAmbientHomeomorph δ hδ) '' segment ℝ a b = segment ℝ ((thinKiteAmbientHomeomorph δ hδ) a) ((thinKiteAmbientHomeomorph δ hδ) b)

The thin-kite homeomorphism is affine on every subsegment of its left base half.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.thinKiteAmbientHomeomorph_image_segment_of_endpoints_mem_rightSpoke (δ : ℝ) (hδ : 0 < δ) {a b : Plane} (ha : a ∈ segment ℝ (planePoint 0 0) (planePoint 1 0)) (hb : b ∈ segment ℝ (planePoint 0 0) (planePoint 1 0)) : ⇑(thinKiteAmbientHomeomorph δ hδ) '' segment ℝ a b = segment ℝ ((thinKiteAmbientHomeomorph δ hδ) a) ((thinKiteAmbientHomeomorph δ hδ) b)

The thin-kite homeomorphism is affine on every subsegment of its right base half.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.baseSegment_eq_spokes : segment ℝ (planePoint (-1) 0) (planePoint 1 0) = segment ℝ (planePoint (-1) 0) (planePoint 0 0) ∪ segment ℝ (planePoint 1 0) (planePoint 0 0)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.thinKiteAmbientHomeomorph_image_baseSegment (δ : ℝ) (hδ : 0 < δ) : ⇑(thinKiteAmbientHomeomorph δ hδ) '' segment ℝ (planePoint (-1) 0) (planePoint 1 0) = segment ℝ (planePoint (-1) 0) (planePoint 0 1) ∪ segment ℝ (planePoint 1 0) (planePoint 0 1)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.thinKiteAmbientHomeomorph_center (δ : ℝ) (hδ : 0 < δ) : (thinKiteAmbientHomeomorph δ hδ) (planePoint 0 0) = planePoint 0 1

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.thinKiteAmbientHomeomorph_eqOn_compl (δ : ℝ) (hδ : 0 < δ) : Set.EqOn (⇑(thinKiteAmbientHomeomorph δ hδ)) id (thinKitePatch δ)ᶜ