Quantitative locally finite PL approximation

This file records the facewise metric control used in Moise Chapter 6, Theorem 3. It is deliberately pointwise: on a noncompact open complex no uniform positive tolerance exists, but a strongly positive tolerance has a positive lower bound on every compact face.

The original face map and the achievable side-control hypotheses

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.vertexPoint_mem_faceCarrier_iff {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (f : K.Face) (v : K.Vertex) : K.vertexPoint v ∈ K.faceCarrier f ↔ v ∈ K.faceVertices f

A global vertex lies in a maximal face carrier exactly when it labels that face.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.vertexSupportPoint_mem_faceInSupport_iff {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (f : K.Face) (v : K.Vertex) : ⟨K.vertexPoint v, ⋯⟩ ∈ PlaneGraphRealization.faceInSupport f ↔ v ∈ K.faceVertices f

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceOriginalMap {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (f : K.Face) (p : Plane) : Plane

The original plane embedding, written in the standard coordinates of one face. Values outside the standard closed triangle are irrelevant.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceOriginalMap_apply {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (f : K.Face) (p : ↑standardFaceRegion) : faceOriginalMap G f ↑p = G.map (PlaneGraphRealization.faceToSupport f ((K.facePlaneHomeomorph f).symm p))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.continuousOn_faceOriginalMap {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (f : K.Face) : ContinuousOn (faceOriginalMap G f) standardFaceRegion

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceOriginalMap_mem_face_image {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (f : K.Face) (p : ↑standardFaceRegion) : faceOriginalMap G f ↑p ∈ G.map '' PlaneGraphRealization.faceInSupport f

def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.FaceBoundariesClose {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (r : K.Face → ℝ) : Prop

The replacement graph is close to the original embedding on each face boundary, with a radius allowed to depend on the face. This is the quantitative hypothesis actually used in Moise's side-preservation argument.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.FaceVertexThickeningsSeparated {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (r : K.Face → ℝ) : Prop

A face-indexed radius separates every nonincident vertex from the original embedded face. The closed-ball/closed-thickening formulation is exactly what the bounded Tietze extension argument consumes.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.outsideVertexImages {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (f : K.Face) : Set Plane

The relatively locally finite set of all vertex images not belonging to one face, made ambiently closed by adjoining the complement of the perturbation region.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.outsideVertexImages G f = (⋃ (v : { v : K.Vertex // v ∉ K.faceVertices f }), G.vertexImageCarrier ↑v) ∪ G.regionᶜ

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.isClosed_outsideVertexImages {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (f : K.Face) : IsClosed (outsideVertexImages G f)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceImage_disjoint_outsideVertexImages {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (f : K.Face) : Disjoint (G.map '' PlaneGraphRealization.faceInSupport f) (outsideVertexImages G f)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.exists_faceVertexSeparationRadius {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (f : K.Face) : ∃ (r : ℝ), 0 < r ∧ ∀ v ∉ K.faceVertices f, Disjoint (Metric.closedBall (G.vertexImage v) r) (Metric.cthickening r (G.map '' PlaneGraphRealization.faceInSupport f))

Every face admits one positive radius separating its compact image from all nonincident vertices at once. Local finiteness replaces the finite minimum used in the compact theorem.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceVertexSeparationRadius {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (f : K.Face) : ℝ

A canonical positive side-separation radius for every face.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceVertexSeparationRadius G f = Classical.choose ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceVertexSeparationRadius_pos {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (f : K.Face) : 0 < faceVertexSeparationRadius G f

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceVertexSeparationRadius_separates {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} : FaceVertexThickeningsSeparated G (faceVertexSeparationRadius G)

The edgewise target for Moise's fine graph subdivision

def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgeMeetingFaces {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (e : K.Edge) : Set K.Face

The finite family of coarse faces meeting an edge. It contains, in particular, every face having that edge as one of its sides.

Equations

• K.edgeMeetingFaces e = {f : K.Face | (K.faceCarrier f ∩ K.edgeCarrier e).Nonempty}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.finite_edgeMeetingFaces {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (e : K.Edge) : (K.edgeMeetingFaces e).Finite

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgeFace_mem_edgeMeetingFaces {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (e : K.Edge) : K.edgeFace e ∈ K.edgeMeetingFaces e

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgeFaceSeparationRadius {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (e : K.Edge) : ℝ

The minimum side-separation radius among the finitely many coarse faces meeting an edge. This is the exact mesh target in Moise Chapter 6, Theorem 2: subdividing the edge until its polygonal replacement is closer than this number preserves the side of every incident face.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgeFaceSeparationRadius_pos {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (e : K.Edge) : 0 < edgeFaceSeparationRadius G e

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgeFaceSeparationRadius_le_of_mem {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {e : K.Edge} {f : K.Face} (hf : f ∈ K.edgeMeetingFaces e) : edgeFaceSeparationRadius G e ≤ faceVertexSeparationRadius G f

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceEdge_mem_edgeMeetingFaces {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (f : K.Face) (i : ZMod 3) : f ∈ K.edgeMeetingFaces (K.faceEdge f i)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceBoundariesClose_of_edgeFaceSeparation_control {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (hsmall : ∀ (e : K.Edge), 2 * Metric.diam (G.edgeImage e) < edgeFaceSeparationRadius G e) : FaceBoundariesClose G (faceVertexSeparationRadius G)

Edgewise diameter control below the incident-face minimum implies the facewise boundary closeness consumed by the side-preservation theorem.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.FaceBoundariesControlled {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (phi : ↑K.support → ℝ) : Prop

The exact facewise estimate needed to control a Schoenflies filling. Every point of a replacement boundary is compared first with its original boundary point and then with an arbitrary point of the same source face.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.FaceOscillationControlled {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (rho phi : ↑K.support → ℝ) : Prop

Separate the graph approximation allowance from the oscillation of the original map on one face. This is the form discharged by an adaptive mesh.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceBoundariesControlled_of_graph_and_oscillation {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {rho phi : ↑K.support → ℝ} (hgraph : G.EdgeImagesControlled rho) (hface : FaceOscillationControlled G rho phi) : FaceBoundariesControlled G phi

Edgewise graph control plus within-face oscillation gives the exact boundary estimate used by every Schoenflies filling.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.facePolygonalCircle_closedRegion_subset_closedBall {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {phi : ↑K.support → ℝ} (hcontrol : FaceBoundariesControlled G phi) (f : K.Face) (p : ↑K.support) (hp : p ∈ PlaneGraphRealization.faceInSupport f) : (facePolygonalCircle f).closedRegion ⊆ Metric.closedBall (G.map p) (phi p)

Under facewise control, the entire polygonal disk selected by Schoenflies lies in the prescribed ball about every point of its source face.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.polygonalReplacementMap_dist_le {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (H : CellwiseCompatibility G) {phi : ↑K.support → ℝ} (hcontrol : FaceBoundariesControlled G phi) (p : ↑K.support) : dist (↑↑(polygonalReplacementMap H p)) (G.map p) ≤ phi p

Pointwise control of the global cellwise replacement.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.SeparatesVerticesFromFaces {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (phi : ↑K.support → ℝ) : Prop

A pointwise tolerance separates nonincident vertices from every source face.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.SeparatesVerticesFromFaces.mono {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {phi psi : ↑K.support → ℝ} (hsep : SeparatesVerticesFromFaces G phi) (hle : ∀ (p : ↑K.support), psi p ≤ phi p) : SeparatesVerticesFromFaces G psi

Any pointwise smaller tolerance inherits vertex-to-face separation.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.finite_setOf_mem_faceInSupport {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (p : ↑K.support) : {f : K.Face | p ∈ PlaneGraphRealization.faceInSupport f}.Finite

Local finiteness leaves only finitely many faces through any one support point.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.mem_faceInSupport_supportFace {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (p : ↑K.support) : p ∈ PlaneGraphRealization.faceInSupport (supportFace p)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.facesContaining {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (p : ↑K.support) : Finset K.Face

The finite set of maximal faces through one support point.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.facesContaining p = ⋯.toFinset

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.mem_facesContaining {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {p : ↑K.support} {f : K.Face} : f ∈ facesContaining p ↔ p ∈ PlaneGraphRealization.faceInSupport f

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.facesContaining_nonempty {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (p : ↑K.support) : (facesContaining p).Nonempty

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.vertexSeparationControl {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) (p : ↑K.support) : ℝ

The pointwise vertex-to-face separation control: the smallest per-face separation radius among the finitely many faces through the point. This is the locally finite analogue of the finite exists_uniform_vertex_face_separation: positive at every point, strongly positive on compact sets, and smaller than the distance from any face through the point to any vertex not incident to that face.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.vertexSeparationControl_le {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {p : ↑K.support} {f : K.Face} (hf : p ∈ PlaneGraphRealization.faceInSupport f) : vertexSeparationControl G p ≤ faceVertexSeparationRadius G f

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.vertexSeparationControl_pos {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (p : ↑K.support) : 0 < vertexSeparationControl G p

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.separatesVerticesFromFaces_vertexSeparationControl {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} : SeparatesVerticesFromFaces G (vertexSeparationControl G)

The canonical control separates every nonincident vertex from every face: each face image is a positive thickening away from the vertex, and the control is below that radius.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.stronglyPositiveOn_vertexSeparationControl {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} : StronglyPositiveOn Set.univ (vertexSeparationControl G)

On every compact set the canonical separation control has a positive lower bound: only finitely many faces meet the compact set, and each contributes a positive radius.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.FaceFillingsVerticesAvoidClosedRegions {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (G : K.PlaneGraphRealization) : Prop

The vertex-side compatibility condition used in Moise's side-preservation argument.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceFillingsVerticesAvoidClosedRegions_of_control {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} {phi : ↑K.support → ℝ} (hcontrol : FaceBoundariesControlled G phi) (hsep : SeparatesVerticesFromFaces G phi) : FaceFillingsVerticesAvoidClosedRegions G

Facewise metric control and vertex-to-face separation keep every nonincident vertex outside the selected polygonal closed disk.