Midpoint subdivision of an intrinsic two-complex

This file constructs the intrinsic 1-to-4 subdivision used to make the source of Moise's PL-approximation theorem fine. A new vertex is attached to every old edge. Each old triangle is then divided into its three corner triangles and its central triangle. Since edge midpoints are indexed by the old edge itself, the construction is automatically coherent across adjacent faces.

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.zmod3_three_add (i : ZMod 3) : 3 + i = i

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.zmod3_add_three (i : ZMod 3) : i + 3 = i

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.zmod3_one_add (i : ZMod 3) : 1 + i = i + 1

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.zmod3_two_add (i : ZMod 3) : 2 + i = i + 2

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.zmod3_add_two_add_one (i : ZMod 3) : i + 2 + 1 = i

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.zmod3_add_one_add_one (i : ZMod 3) : i + 1 + 1 = i + 2

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.zmod3_add_one_add_two (i : ZMod 3) : i + 1 + 2 = i

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.zmod3_add_two_add_two (i : ZMod 3) : i + 2 + 2 = i + 1

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.MidpointVertex (K : IntrinsicTwoComplex) : Type

Vertices of the midpoint subdivision: old vertices and one new vertex for every old edge.

Equations

• K.MidpointVertex = (K.Vertex ⊕ K.Edge)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointCornerFace (K : IntrinsicTwoComplex) (t : K.Face) (i : ZMod 3) : Finset K.MidpointVertex

The corner triangle at the i-th vertex of an old face.

Equations

• K.midpointCornerFace t i = {Sum.inl (K.faceVertex t i), Sum.inr (K.faceEdge t i), Sum.inr (K.faceEdge t (i + 2))}

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointCentralFace (K : IntrinsicTwoComplex) (t : K.Face) : Finset K.MidpointVertex

The central triangle of the midpoint subdivision of an old face.

Equations

• K.midpointCentralFace t = Finset.image (fun (i : ZMod 3) => Sum.inr (K.faceEdge t i)) Finset.univ

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointFacesOver (K : IntrinsicTwoComplex) (t : K.Face) : Finset (Finset K.MidpointVertex)

The four midpoint triangles belonging to one old face.

Equations

• K.midpointFacesOver t = Finset.image (K.midpointCornerFace t) Finset.univ ∪ {K.midpointCentralFace t}

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointFaces (K : IntrinsicTwoComplex) : Finset (Finset K.MidpointVertex)

All maximal faces in the midpoint subdivision.

Equations

• K.midpointFaces = K.faces.attach.biUnion K.midpointFacesOver

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceEdge_ne_add_two (K : IntrinsicTwoComplex) (t : K.Face) (i : ZMod 3) : K.faceEdge t i ≠ K.faceEdge t (i + 2)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceEdge_injective (K : IntrinsicTwoComplex) (t : K.Face) : Function.Injective (K.faceEdge t)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointCornerFace_card (K : IntrinsicTwoComplex) (t : K.Face) (i : ZMod 3) : (K.midpointCornerFace t i).card = 3

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointCentralFace_card (K : IntrinsicTwoComplex) (t : K.Face) : (K.midpointCentralFace t).card = 3

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointFacesOver_card (K : IntrinsicTwoComplex) (t : K.Face) {s : Finset K.MidpointVertex} (hs : s ∈ K.midpointFacesOver t) : s.card = 3

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointComplex (K : IntrinsicTwoComplex) : IntrinsicTwoComplex

The finite abstract complex underlying midpoint subdivision.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointComplex_faces (K : IntrinsicTwoComplex) : K.midpointComplex.faces = K.midpointFaces

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.exists_parentFace_of_mem_midpointFaces (K : IntrinsicTwoComplex) {s : Finset K.MidpointVertex} (hs : s ∈ K.midpointFaces) : ∃ (t : K.Face), s ∈ K.midpointFacesOver t

Every refined face remembers an old face which contains it geometrically.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointParentFace (K : IntrinsicTwoComplex) (s : K.midpointComplex.Face) : K.Face

A chosen parent of a midpoint-subdivision face. Geometric arguments use only midpointFace_mem_parent; uniqueness is not needed for the adaptive open-complex construction.

Equations

• K.midpointParentFace s = Classical.choose ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointFace_mem_parent (K : IntrinsicTwoComplex) (s : K.midpointComplex.Face) : ↑s ∈ K.midpointFacesOver (K.midpointParentFace s)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointPosition (K : IntrinsicTwoComplex) : K.MidpointVertex → K.Vertex → ℝ

Canonical old barycentric position of a midpoint-subdivision vertex.

Equations

• K.midpointPosition (Sum.inl v) = Pi.single v 1
• K.midpointPosition (Sum.inr e) = fun (v : K.Vertex) => if v ∈ ↑e then 2⁻¹ else 0

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointPosition_old (K : IntrinsicTwoComplex) (v : K.Vertex) : K.midpointPosition (Sum.inl v) = Pi.single v 1

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointPosition_edge_apply (K : IntrinsicTwoComplex) (e : K.Edge) (v : K.Vertex) : K.midpointPosition (Sum.inr e) v = if v ∈ ↑e then 2⁻¹ else 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointPosition_nonneg (K : IntrinsicTwoComplex) (w : K.MidpointVertex) (u : K.Vertex) : 0 ≤ K.midpointPosition w u

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.sum_midpointPosition (K : IntrinsicTwoComplex) (w : K.MidpointVertex) : ∑ v : K.Vertex, K.midpointPosition w v = 1

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointEvalAffine (K : IntrinsicTwoComplex) : (K.MidpointVertex → ℝ) →ᵃ[ℝ] K.Vertex → ℝ

Affine barycentric evaluation from midpoint coordinates to old coordinates.

Equations

• K.midpointEvalAffine = (∑ w : K.MidpointVertex, (LinearMap.proj w).smulRight (K.midpointPosition w)).toAffineMap

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointEvalAffine_apply (K : IntrinsicTwoComplex) (x : K.MidpointVertex → ℝ) : K.midpointEvalAffine x = ∑ w : K.MidpointVertex, x w • K.midpointPosition w

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointEvalAffine_eq_sum_of_support (K : IntrinsicTwoComplex) {x : K.MidpointVertex → ℝ} {s : Finset K.MidpointVertex} (hsupp : ∀ w ∉ s, x w = 0) : K.midpointEvalAffine x = ∑ w ∈ s, x w • K.midpointPosition w

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.sum_eq_sum_of_midpointSupport (K : IntrinsicTwoComplex) {x : K.MidpointVertex → ℝ} {s : Finset K.MidpointVertex} (hsupp : ∀ w ∉ s, x w = 0) : ∑ w : K.MidpointVertex, x w = ∑ w ∈ s, x w

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.exists_faceVertex_eq_of_mem (K : IntrinsicTwoComplex) (t : K.Face) {v : K.Vertex} (hv : v ∈ ↑t) : ∃ (i : ZMod 3), K.faceVertex t i = v

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointCentralFace_eq (K : IntrinsicTwoComplex) (t : K.Face) (i : ZMod 3) : K.midpointCentralFace t = {Sum.inr (K.faceEdge t i), Sum.inr (K.faceEdge t (i + 1)), Sum.inr (K.faceEdge t (i + 2))}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointEval_corner_self (K : IntrinsicTwoComplex) (t : K.Face) (i : ZMod 3) {x : K.MidpointVertex → ℝ} (hx : ∀ w ∉ K.midpointCornerFace t i, x w = 0) : K.midpointEvalAffine x (K.faceVertex t i) = x (Sum.inl (K.faceVertex t i)) + (x (Sum.inr (K.faceEdge t i)) + x (Sum.inr (K.faceEdge t (i + 2)))) / 2

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointEval_corner_next (K : IntrinsicTwoComplex) (t : K.Face) (i : ZMod 3) {x : K.MidpointVertex → ℝ} (hx : ∀ w ∉ K.midpointCornerFace t i, x w = 0) : K.midpointEvalAffine x (K.faceVertex t (i + 1)) = x (Sum.inr (K.faceEdge t i)) / 2

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointEval_corner_prev (K : IntrinsicTwoComplex) (t : K.Face) (i : ZMod 3) {x : K.MidpointVertex → ℝ} (hx : ∀ w ∉ K.midpointCornerFace t i, x w = 0) : K.midpointEvalAffine x (K.faceVertex t (i + 2)) = x (Sum.inr (K.faceEdge t (i + 2))) / 2

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointEval_central_coord (K : IntrinsicTwoComplex) (t : K.Face) (i : ZMod 3) {x : K.MidpointVertex → ℝ} (hx : ∀ w ∉ K.midpointCentralFace t, x w = 0) : K.midpointEvalAffine x (K.faceVertex t i) = (x (Sum.inr (K.faceEdge t i)) + x (Sum.inr (K.faceEdge t (i + 2)))) / 2

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointRecoverOld (K : IntrinsicTwoComplex) (p : K.Vertex → ℝ) (v : K.Vertex) : ℝ

Coefficient of an old vertex recovered from a point of the subdivided simplex.

Equations

• K.midpointRecoverOld p v = max (2 * p v - 1) 0

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointRecoverEdge (K : IntrinsicTwoComplex) (p : K.Vertex → ℝ) (e : K.Edge) : ℝ

Coefficient of an edge midpoint recovered from old barycentric coordinates. The formula is symmetric in the two endpoints despite the arbitrary endpoint ordering.

Equations

• K.midpointRecoverEdge p e = max 0 (min (2 * p (K.edgeFirst e)) (min (2 * p (K.edgeSecond e)) (2 * (p (K.edgeFirst e) + p (K.edgeSecond e)) - 1)))

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointRecover (K : IntrinsicTwoComplex) (p : K.Vertex → ℝ) : K.MidpointVertex → ℝ

The inverse-coordinate formula for midpoint evaluation.

Equations

• K.midpointRecover p (Sum.inl v) = K.midpointRecoverOld p v
• K.midpointRecover p (Sum.inr e) = K.midpointRecoverEdge p e

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointRecoverEdge_faceEdge (K : IntrinsicTwoComplex) (p : K.Vertex → ℝ) (t : K.Face) (i : ZMod 3) : K.midpointRecoverEdge p (K.faceEdge t i) = max 0 (min (2 * p (K.faceVertex t i)) (min (2 * p (K.faceVertex t (i + 1))) (2 * (p (K.faceVertex t i) + p (K.faceVertex t (i + 1))) - 1)))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.exists_faceEdge_eq_of_subset (K : IntrinsicTwoComplex) (t : K.Face) (e : K.Edge) (het : ↑e ⊆ ↑t) : ∃ (i : ZMod 3), K.faceEdge t i = e

Every old edge contained in a face is one of its three cyclic edges.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceEdge_subset_face (K : IntrinsicTwoComplex) (t : K.Face) (i : ZMod 3) : ↑(K.faceEdge t i) ⊆ ↑t

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointPosition_support_of_mem_face (K : IntrinsicTwoComplex) (t : K.Face) {s : Finset K.MidpointVertex} (hs : s ∈ K.midpointFacesOver t) {w : K.MidpointVertex} (hw : w ∈ s) {v : K.Vertex} (hv : v ∉ ↑t) : K.midpointPosition w v = 0

Every vertex of a refined face is supported on its parent old face.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointEvalAffine_support (K : IntrinsicTwoComplex) (t : K.Face) {s : Finset K.MidpointVertex} (hs : s ∈ K.midpointFacesOver t) {x : K.MidpointVertex → ℝ} (hxs : ∀ w ∉ s, x w = 0) {v : K.Vertex} (hv : v ∉ ↑t) : K.midpointEvalAffine x v = 0

The affine midpoint evaluation sends a refined face into its parent old face.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.exists_midpointPosition_pos_of_mem_parent (K : IntrinsicTwoComplex) (t : K.Face) {s : Finset K.MidpointVertex} (hs : s ∈ K.midpointFacesOver t) {v : K.Vertex} (hv : v ∈ ↑t) : ∃ w ∈ s, 0 < K.midpointPosition w v

Every old vertex of a parent face receives positive weight from at least one vertex of each midpoint child.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointEvalAffine_pos_on_parent (K : IntrinsicTwoComplex) (t : K.Face) {s : Finset K.MidpointVertex} (hs : s ∈ K.midpointFacesOver t) {x : K.MidpointVertex → ℝ} (hxs : ∀ w ∉ s, x w = 0) (hx0 : ∀ (w : K.MidpointVertex), 0 ≤ x w) (hxpos : ∀ w ∈ s, 0 < x w) {v : K.Vertex} (hv : v ∈ ↑t) : 0 < K.midpointEvalAffine x v

A point with strictly positive coordinates on a midpoint child maps to a point with strictly positive coordinates on its parent.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointFacesOver_parent_unique (K : IntrinsicTwoComplex) {t u : K.Face} {s : Finset K.MidpointVertex} (hst : s ∈ K.midpointFacesOver t) (hsu : s ∈ K.midpointFacesOver u) : t = u

A midpoint child has a unique old parent triangle.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointFacesOver_mixed_edge_card_le_one (K : IntrinsicTwoComplex) (t : K.Face) (v : K.Vertex) (e : K.Edge) : {s ∈ K.midpointFacesOver t | {Sum.inl v, Sum.inr e} ⊆ s}.card ≤ 1

Inside one old parent, a refined edge joining an old vertex to an old-edge midpoint belongs to at most one midpoint child.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edge_subset_parent_of_midpoint_mem (K : IntrinsicTwoComplex) (t : K.Face) {s : Finset K.MidpointVertex} (hs : s ∈ K.midpointFacesOver t) (e : K.Edge) (he : Sum.inr e ∈ s) : ↑e ⊆ ↑t

An old edge whose midpoint occurs in a midpoint child belongs to that child's parent.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.oldVertex_eq_of_mem_midpointFace (K : IntrinsicTwoComplex) (t : K.Face) {s : Finset K.MidpointVertex} (hs : s ∈ K.midpointFacesOver t) {v w : K.Vertex} (hv : Sum.inl v ∈ s) (hw : Sum.inl w ∈ s) : v = w

A midpoint child contains at most one old vertex.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceEdge_union_eq_face_of_ne (K : IntrinsicTwoComplex) (t : K.Face) {i j : ZMod 3} (hij : i ≠ j) : ↑(K.faceEdge t i) ∪ ↑(K.faceEdge t j) = ↑t

Two distinct edges of a triangular face cover the whole face.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.face_eq_of_two_edges_subset (K : IntrinsicTwoComplex) {t u : K.Face} {e d : K.Edge} (hed : e ≠ d) (het : ↑e ⊆ ↑t) (hdt : ↑d ⊆ ↑t) (heu : ↑e ⊆ ↑u) (hdu : ↑d ⊆ ↑u) : t = u

Two distinct old edges determine their triangular parent.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointCornerFace_eq_of_two_midpoints_mem (K : IntrinsicTwoComplex) (t : K.Face) {i j : ZMod 3} {e d : K.Edge} (hed : e ≠ d) (hei : Sum.inr e ∈ K.midpointCornerFace t i) (hdi : Sum.inr d ∈ K.midpointCornerFace t i) (hej : Sum.inr e ∈ K.midpointCornerFace t j) (hdj : Sum.inr d ∈ K.midpointCornerFace t j) : K.midpointCornerFace t i = K.midpointCornerFace t j

In a fixed parent, two distinct midpoint vertices determine at most one corner child.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointCornerFaces_pair_card_le_one (K : IntrinsicTwoComplex) (t : K.Face) (e d : K.Edge) (hed : e ≠ d) : {s ∈ Finset.image (K.midpointCornerFace t) Finset.univ | {Sum.inr e, Sum.inr d} ⊆ s}.card ≤ 1

Within one old parent, the corner children incident to two distinct midpoint vertices form a set of cardinality at most one.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointFacesOver_midpoint_edge_card_le_two (K : IntrinsicTwoComplex) (t : K.Face) (e d : K.Edge) (hed : e ≠ d) : {s ∈ K.midpointFacesOver t | {Sum.inr e, Sum.inr d} ⊆ s}.card ≤ 2

Inside one old parent, a refined edge joining two old-edge midpoints belongs to at most two midpoint children (one corner and the central child).

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpoint_mixed_edge_valence (K : IntrinsicTwoComplex) (hK : K.HasSurfaceEdgeValence) (v : K.Vertex) (e : K.Edge) : {s ∈ K.midpointComplex.faces | {Sum.inl v, Sum.inr e} ⊆ s}.card ≤ 2

Globally, a mixed old-vertex/midpoint edge inherits the valence bound of its old edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpoint_mixed_edge_valence_of_eq (K : IntrinsicTwoComplex) (hK : K.HasSurfaceEdgeValence) (v : K.Vertex) (e : K.Edge) (q : Finset K.MidpointVertex) (hq : q = {Sum.inl v, Sum.inr e}) : {s ∈ K.midpointComplex.faces | q ⊆ s}.card ≤ 2

Equality-normalized form of midpoint_mixed_edge_valence, convenient when the two endpoints of the unordered edge are presented in the opposite order.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpoint_midpoint_edge_valence (K : IntrinsicTwoComplex) (e d : K.Edge) (hed : e ≠ d) : {s ∈ K.midpointComplex.faces | {Sum.inr e, Sum.inr d} ⊆ s}.card ≤ 2

Globally, an edge joining two distinct old-edge midpoints is contained in at most two midpoint children. The two old edges determine a single parent triangle.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.hasSurfaceEdgeValence_midpointComplex (K : IntrinsicTwoComplex) (hK : K.HasSurfaceEdgeValence) : K.midpointComplex.HasSurfaceEdgeValence

Midpoint subdivision preserves the surface edge-valence bound.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointRecoverOld_corner (K : IntrinsicTwoComplex) (t : K.Face) (i : ZMod 3) {x : K.MidpointVertex → ℝ} (hx : ∀ w ∉ K.midpointCornerFace t i, x w = 0) (hx0 : ∀ (w : K.MidpointVertex), 0 ≤ x w) (hx1 : ∑ w : K.MidpointVertex, x w = 1) (v : K.Vertex) : K.midpointRecoverOld (K.midpointEvalAffine x) v = x (Sum.inl v)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointRecoverOld_central (K : IntrinsicTwoComplex) (t : K.Face) {x : K.MidpointVertex → ℝ} (hx : ∀ w ∉ K.midpointCentralFace t, x w = 0) (hx0 : ∀ (w : K.MidpointVertex), 0 ≤ x w) (hx1 : ∑ w : K.MidpointVertex, x w = 1) (v : K.Vertex) : K.midpointRecoverOld (K.midpointEvalAffine x) v = x (Sum.inl v)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointRecoverEdge_corner (K : IntrinsicTwoComplex) (t : K.Face) (i : ZMod 3) {x : K.MidpointVertex → ℝ} (hx : ∀ w ∉ K.midpointCornerFace t i, x w = 0) (hx0 : ∀ (w : K.MidpointVertex), 0 ≤ x w) (hx1 : ∑ w : K.MidpointVertex, x w = 1) (e : K.Edge) : K.midpointRecoverEdge (K.midpointEvalAffine x) e = x (Sum.inr e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointRecoverEdge_central (K : IntrinsicTwoComplex) (t : K.Face) {x : K.MidpointVertex → ℝ} (hx : ∀ w ∉ K.midpointCentralFace t, x w = 0) (hx0 : ∀ (w : K.MidpointVertex), 0 ≤ x w) (hx1 : ∑ w : K.MidpointVertex, x w = 1) (e : K.Edge) : K.midpointRecoverEdge (K.midpointEvalAffine x) e = x (Sum.inr e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointRecover_midpointEvalAffine (K : IntrinsicTwoComplex) (x : K.midpointComplex.realization) : K.midpointRecover (K.midpointEvalAffine ↑x) = ↑x

Midpoint coordinates are uniquely recovered from their old barycentric image.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.injective_midpointEvalAffine_on_realization (K : IntrinsicTwoComplex) : Function.Injective fun (x : K.midpointComplex.realization) => K.midpointEvalAffine ↑x

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.face_eq_image_faceVertex (K : IntrinsicTwoComplex) (t : K.Face) : ↑t = Finset.image (K.faceVertex t) Finset.univ

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.sum_faceVertex_coords (K : IntrinsicTwoComplex) (t : K.Face) (p : K.Vertex → ℝ) (hsupp : ∀ v ∉ ↑t, p v = 0) (hsum : ∑ v : K.Vertex, p v = 1) (i : ZMod 3) : p (K.faceVertex t i) + p (K.faceVertex t (i + 1)) + p (K.faceVertex t (i + 2)) = 1

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointCornerWeights (K : IntrinsicTwoComplex) (t : K.Face) (i : ZMod 3) (p : K.Vertex → ℝ) : K.MidpointVertex → ℝ

Explicit inverse coordinates in a corner triangle.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointCornerWeights_old (K : IntrinsicTwoComplex) (t : K.Face) (i : ZMod 3) (p : K.Vertex → ℝ) : K.midpointCornerWeights t i p (Sum.inl (K.faceVertex t i)) = 2 * p (K.faceVertex t i) - 1

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointCornerWeights_nextEdge (K : IntrinsicTwoComplex) (t : K.Face) (i : ZMod 3) (p : K.Vertex → ℝ) : K.midpointCornerWeights t i p (Sum.inr (K.faceEdge t i)) = 2 * p (K.faceVertex t (i + 1))

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointCornerWeights_prevEdge (K : IntrinsicTwoComplex) (t : K.Face) (i : ZMod 3) (p : K.Vertex → ℝ) : K.midpointCornerWeights t i p (Sum.inr (K.faceEdge t (i + 2))) = 2 * p (K.faceVertex t (i + 2))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointCornerWeights_support (K : IntrinsicTwoComplex) (t : K.Face) (i : ZMod 3) (p : K.Vertex → ℝ) (w : K.MidpointVertex) : w ∉ K.midpointCornerFace t i → K.midpointCornerWeights t i p w = 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointCornerWeights_nonneg (K : IntrinsicTwoComplex) (t : K.Face) (i : ZMod 3) (p : K.Vertex → ℝ) (hp0 : ∀ (v : K.Vertex), 0 ≤ p v) (hi : 2⁻¹ ≤ p (K.faceVertex t i)) (w : K.MidpointVertex) : 0 ≤ K.midpointCornerWeights t i p w

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.sum_midpointCornerWeights (K : IntrinsicTwoComplex) (t : K.Face) (i : ZMod 3) (p : K.Vertex → ℝ) (hsum : p (K.faceVertex t i) + p (K.faceVertex t (i + 1)) + p (K.faceVertex t (i + 2)) = 1) : ∑ w : K.MidpointVertex, K.midpointCornerWeights t i p w = 1

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointCentralWeights (K : IntrinsicTwoComplex) (t : K.Face) (p : K.Vertex → ℝ) : K.MidpointVertex → ℝ

Explicit inverse coordinates in the central triangle.

Equations

• K.midpointCentralWeights t p w = ∑ i : ZMod 3, if w = Sum.inr (K.faceEdge t i) then 1 - 2 * p (K.faceVertex t (i + 2)) else 0

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointCentralWeights_edge (K : IntrinsicTwoComplex) (t : K.Face) (p : K.Vertex → ℝ) (i : ZMod 3) : K.midpointCentralWeights t p (Sum.inr (K.faceEdge t i)) = 1 - 2 * p (K.faceVertex t (i + 2))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointCentralWeights_support (K : IntrinsicTwoComplex) (t : K.Face) (p : K.Vertex → ℝ) (w : K.MidpointVertex) : w ∉ K.midpointCentralFace t → K.midpointCentralWeights t p w = 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointCentralWeights_nonneg (K : IntrinsicTwoComplex) (t : K.Face) (p : K.Vertex → ℝ) (hle : ∀ (i : ZMod 3), p (K.faceVertex t i) ≤ 2⁻¹) (w : K.MidpointVertex) : 0 ≤ K.midpointCentralWeights t p w

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.sum_midpointCentralWeights (K : IntrinsicTwoComplex) (t : K.Face) (p : K.Vertex → ℝ) (hsum : p (K.faceVertex t 0) + p (K.faceVertex t 1) + p (K.faceVertex t 2) = 1) : ∑ w : K.MidpointVertex, K.midpointCentralWeights t p w = 1

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.exists_midpoint_preimage_in_face (K : IntrinsicTwoComplex) (T : K.Face) (p : K.realization) (hpt : p ∈ K.faceCarrier ↑T) : ∃ (x : K.midpointComplex.realization), ∃ s ∈ K.midpointFacesOver T, x ∈ K.midpointComplex.faceCarrier s ∧ K.midpointEvalAffine ↑x = ↑p

The four named midpoint children of an old face cover that old face.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.surjective_midpointEvalAffine_on_realization (K : IntrinsicTwoComplex) (p : K.realization) : ∃ (x : K.midpointComplex.realization), K.midpointEvalAffine ↑x = ↑p

The four midpoint triangles cover every old face, hence the whole realization.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointEvalAffine_nonneg (K : IntrinsicTwoComplex) (x : K.midpointComplex.realization) (v : K.Vertex) : 0 ≤ K.midpointEvalAffine (↑x) v

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.sum_midpointEvalAffine (K : IntrinsicTwoComplex) (x : K.midpointComplex.realization) : ∑ v : K.Vertex, K.midpointEvalAffine (↑x) v = 1

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointEval (K : IntrinsicTwoComplex) (x : K.midpointComplex.realization) : K.realization

Canonical affine map from the midpoint realization into the old realization.

Equations

• K.midpointEval x = ⟨K.midpointEvalAffine ↑x, ⋯⟩

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointEval_val (K : IntrinsicTwoComplex) (x : K.midpointComplex.realization) : ↑(K.midpointEval x) = K.midpointEvalAffine ↑x

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.continuous_midpointEval (K : IntrinsicTwoComplex) : Continuous K.midpointEval

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointEval_mem_parentFace (K : IntrinsicTwoComplex) (t : K.Face) {s : Finset K.MidpointVertex} (hs : s ∈ K.midpointFacesOver t) (x : K.midpointComplex.realization) (hx : x ∈ K.midpointComplex.faceCarrier s) : K.midpointEval x ∈ K.faceCarrier ↑t

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointEval_affineOnFace (K : IntrinsicTwoComplex) {s : Finset K.MidpointVertex} : s ∈ K.midpointFaces → ∃ (a : (K.MidpointVertex → ℝ) →ᵃ[ℝ] K.Vertex → ℝ), ∀ x ∈ K.midpointComplex.faceCarrier s, ↑(K.midpointEval x) = a ↑x

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.injective_midpointEval (K : IntrinsicTwoComplex) : Function.Injective K.midpointEval

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.surjective_midpointEval (K : IntrinsicTwoComplex) : Function.Surjective K.midpointEval

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointHomeomorph (K : IntrinsicTwoComplex) : K.midpointComplex.realization ≃ₜ K.realization

The canonical midpoint realization map is a homeomorphism.

Equations

• K.midpointHomeomorph = ⋯.homeoOfEquivCompactToT2

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointHomeomorph_apply (K : IntrinsicTwoComplex) (x : K.midpointComplex.realization) : K.midpointHomeomorph x = K.midpointEval x

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointSubdivision (K : IntrinsicTwoComplex) : K.Subdivision

The intrinsic 1-to-4 midpoint subdivision, with its canonical faithful realization map.

Equations

• K.midpointSubdivision = { refined := K.midpointComplex, homeo := K.midpointHomeomorph, affineOnFace := ⋯, subordinate := ⋯ }

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointSubdivision_refined (K : IntrinsicTwoComplex) : K.midpointSubdivision.refined = K.midpointComplex

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointSubdivision_homeo_apply (K : IntrinsicTwoComplex) (x : K.midpointComplex.realization) : K.midpointSubdivision.homeo x = K.midpointEval x