Adaptive meshes for strongly-positive metric controls

Moise Chapter 6 first subdivides the source until every simplex is small compared with the prescribed strongly-positive tolerance. This file supplies that step for the locally finite adaptive triangulation. Strong positivity gives a uniform lower bound on a compact neighborhood of each point; continuity then shrinks that neighborhood until its image has small diameter. Subordination to the resulting open cover converts the existing setwise polygonal graph replacement into a pointwise controlled approximation.

structure LeanEval.Topology.ClassificationOfSurfaces.Moise.ControlledNeighborhood {X : Type u_1} [TopologicalSpace X] (f : X → Plane) (phi : X → ℝ) (x : X) : Type u_1

A neighborhood on which phi has a fixed positive lower bound and the image of f has diameter at most one quarter of that bound.

• set : Set X

  The set declaration.

• isOpen : IsOpen self.set
• mem_set : x ∈ self.set
• scale : ℝ

  The scale declaration.

• scale_pos : 0 < self.scale
• scale_le_one : self.scale ≤ 1
• scale_le (y : X) : y ∈ self.set → self.scale ≤ phi y
• dist_le_quarter (y : X) : y ∈ self.set → ∀ z ∈ self.set, dist (f y) (f z) ≤ self.scale / 4

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.exists_controlledNeighborhood {X : Type u_1} [TopologicalSpace X] [LocallyCompactSpace X] {f : X → Plane} (hf : Continuous f) {phi : X → ℝ} (hphi : StronglyPositiveOn Set.univ phi) (x : X) : Nonempty (ControlledNeighborhood f phi x)

Strong positivity and local compactness produce controlled neighborhoods for every point.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.controlledNeighborhood {X : Type u_1} [TopologicalSpace X] [LocallyCompactSpace X] {f : X → Plane} (hf : Continuous f) {phi : X → ℝ} (hphi : StronglyPositiveOn Set.univ phi) (x : X) : ControlledNeighborhood f phi x

A chosen controlled neighborhood at every point.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.controlledNeighborhood hf hphi x = Classical.choice ⋯

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.regionMeshControl {X : Type u_1} (V : Set Plane) (f : X → Plane) (x : X) : ℝ

The part of a mesh tolerance reserved for staying inside an open target region. When the region is all of the plane, the constant bound 1 is used instead.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.regionMeshControl V f x = if hcomp : Vᶜ.Nonempty then min 1 (LeanEval.Topology.ClassificationOfSurfaces.Moise.frontierDistance V (f x) / 4) else 1

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.regionMeshControl_le_one {X : Type u_1} (V : Set Plane) (f : X → Plane) (x : X) : regionMeshControl V f x ≤ 1

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.regionMeshControl_le_frontier {X : Type u_1} {V : Set Plane} (hcomp : Vᶜ.Nonempty) (f : X → Plane) (x : X) : regionMeshControl V f x ≤ frontierDistance V (f x) / 4

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.stronglyPositiveOn_regionMeshControl {X : Type u_1} [TopologicalSpace X] {V : Set Plane} (hV : IsOpen V) {f : X → Plane} (hf : Continuous f) (hmem : ∀ (x : X), f x ∈ V) : StronglyPositiveOn Set.univ (regionMeshControl V f)

The target-region mesh control is strongly positive along any continuous map landing in that region.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.regionSafeControl {X : Type u_1} (V : Set Plane) (f : X → Plane) (phi : X → ℝ) (x : X) : ℝ

Combine a requested approximation tolerance with the target-region mesh control.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.regionSafeControl V f phi x = min (phi x) (LeanEval.Topology.ClassificationOfSurfaces.Moise.regionMeshControl V f x)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.regionSafeControl_le_left {X : Type u_1} (V : Set Plane) (f : X → Plane) (phi : X → ℝ) (x : X) : regionSafeControl V f phi x ≤ phi x

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.regionSafeControl_le_one {X : Type u_1} (V : Set Plane) (f : X → Plane) (phi : X → ℝ) (x : X) : regionSafeControl V f phi x ≤ 1

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.regionSafeControl_le_frontier {X : Type u_1} {V : Set Plane} (hcomp : Vᶜ.Nonempty) (f : X → Plane) (phi : X → ℝ) (x : X) : regionSafeControl V f phi x ≤ frontierDistance V (f x) / 4

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.StronglyPositiveOn.min_control {X : Type u_1} [TopologicalSpace X] {U : Set X} {phi psi : X → ℝ} (hphi : StronglyPositiveOn U phi) (hpsi : StronglyPositiveOn U psi) : StronglyPositiveOn U fun (x : X) => min (phi x) (psi x)

A minimum of two strongly-positive controls is strongly positive.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.stronglyPositiveOn_regionSafeControl {X : Type u_1} [TopologicalSpace X] {V : Set Plane} (hV : IsOpen V) {f : X → Plane} (hf : Continuous f) (hmem : ∀ (x : X), f x ∈ V) {phi : X → ℝ} (hphi : StronglyPositiveOn Set.univ phi) : StronglyPositiveOn Set.univ (regionSafeControl V f phi)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.controlledAdaptiveOpenCover (K : IntrinsicTwoComplex) (U : Set K.realization) (hU : IsOpen U) (f : ↑U → Plane) (hf : Continuous f) (phi : ↑U → ℝ) (hphi : StronglyPositiveOn Set.univ phi) : K.AdaptiveOpenCover U

The ambient open cover obtained from controlled neighborhoods in the open subspace U.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.ControlledAdaptiveOpenCover.cover_set_control (K : IntrinsicTwoComplex) (U : Set K.realization) (hU : IsOpen U) (f : ↑U → Plane) (hf : Continuous f) (phi : ↑U → ℝ) (hphi : StronglyPositiveOn Set.univ phi) (x : ↑U) : ∃ (eps : ℝ), 0 < eps ∧ eps ≤ 1 ∧ (∀ (y : ↑U), ↑y ∈ (K.controlledAdaptiveOpenCover U hU f hf phi hphi).set x → eps ≤ phi y) ∧ ∀ (y z : ↑U), ↑y ∈ (K.controlledAdaptiveOpenCover U hU f hf phi hphi).set x → ↑z ∈ (K.controlledAdaptiveOpenCover U hU f hf phi hphi).set x → dist (f y) (f z) ≤ eps / 4

Every selected cover set retains its quantitative scale and image-diameter bounds.

@[reducible, inline]

noncomputable abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.controlledAdaptiveComplex (K : IntrinsicTwoComplex) (U : Set K.realization) (hU : IsOpen U) (f : ↑U → Plane) (hf : Continuous f) (phi : ↑U → ℝ) (hphi : StronglyPositiveOn Set.univ phi) : LocallyFiniteTriangleComplex ↑U

The adaptive locally finite triangle complex subordinate to the quantitative cover.

Equations

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

@[reducible, inline]

noncomputable abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.regionControlledAdaptiveComplex (K : IntrinsicTwoComplex) (U : Set K.realization) (hU : IsOpen U) (V : Set Plane) (hV : IsOpen V) (f : ↑U → Plane) (hf : Continuous f) (hmem : ∀ (x : ↑U), f x ∈ V) (phi : ↑U → ℝ) (hphi : StronglyPositiveOn Set.univ phi) : LocallyFiniteTriangleComplex ↑U

The controlled adaptive complex with its tolerance automatically reduced near the frontier of an open target region.

Equations

• K.regionControlledAdaptiveComplex U hU V hV f hf hmem phi hphi = K.controlledAdaptiveComplex U hU f hf (LeanEval.Topology.ClassificationOfSurfaces.Moise.regionSafeControl V f phi) ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.ControlledAdaptiveComplex.exists_face_scale (K : IntrinsicTwoComplex) (U : Set K.realization) (hU : IsOpen U) (f : ↑U → Plane) (hf : Continuous f) (phi : ↑U → ℝ) (hphi : StronglyPositiveOn Set.univ phi) (t : (LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.ControlledAdaptiveComplex.L✝ K U hU f hf phi hphi).Face) : ∃ (eps : ℝ), 0 < eps ∧ eps ≤ 1 ∧ (∀ p ∈ (LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.ControlledAdaptiveComplex.L✝ K U hU f hf phi hphi).faceCarrier t, eps ≤ phi p) ∧ ∀ (p q : ↑U), p ∈ (LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.ControlledAdaptiveComplex.L✝ K U hU f hf phi hphi).faceCarrier t → q ∈ (LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.ControlledAdaptiveComplex.L✝ K U hU f hf phi hphi).faceCarrier t → dist (f p) (f q) ≤ eps / 4

Each adaptive face inherits one quantitative scale from the cover member containing it.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.ControlledAdaptiveComplex.edgeImagesControlled (K : IntrinsicTwoComplex) (U : Set K.realization) (hU : IsOpen U) (f : ↑U → Plane) (hf : Continuous f) (phi : ↑U → ℝ) (hphi : StronglyPositiveOn Set.univ phi) (G : (LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.ControlledAdaptiveComplex.L✝ K U hU f hf phi hphi).PlaneGraphRealization) (hmap : ∀ (p : ↑(LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.ControlledAdaptiveComplex.L✝ K U hU f hf phi hphi).support), G.map p = f ↑p) : G.EdgeImagesControlled fun (p : ↑(LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.ControlledAdaptiveComplex.L✝ K U hU f hf phi hphi).support) => phi ↑p

Subordination makes every edge image small enough for the canonical simultaneous polygonal replacement to satisfy the original strongly-positive pointwise control.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.ControlledAdaptiveComplex.isPhiApproximation_graphReplacementMap (K : IntrinsicTwoComplex) (U : Set K.realization) (hU : IsOpen U) (f : ↑U → Plane) (hf : Continuous f) (phi : ↑U → ℝ) (hphi : StronglyPositiveOn Set.univ phi) (G : (LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.ControlledAdaptiveComplex.L✝ K U hU f hf phi hphi).PlaneGraphRealization) (hmap : ∀ (p : ↑(LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.ControlledAdaptiveComplex.L✝ K U hU f hf phi hphi).support), G.map p = f ↑p) (p : ↑LocallyFiniteTriangleComplex.PlaneGraphRealization.oneSkeletonInSupport) : dist (G.graphReplacementMap p) (f ↑↑p) < phi ↑↑p

The canonical replacement graph on the controlled adaptive mesh is a pointwise phi-approximation of the original realization.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.ControlledAdaptiveComplex.edgeImage_diam_le_face_scale (K : IntrinsicTwoComplex) (U : Set K.realization) (hU : IsOpen U) (f : ↑U → Plane) (hf : Continuous f) (phi : ↑U → ℝ) (hphi : StronglyPositiveOn Set.univ phi) (G : (LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.ControlledAdaptiveComplex.L✝ K U hU f hf phi hphi).PlaneGraphRealization) (hmap : ∀ (p : ↑(LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.ControlledAdaptiveComplex.L✝ K U hU f hf phi hphi).support), G.map p = f ↑p) (t : (LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.ControlledAdaptiveComplex.L✝ K U hU f hf phi hphi).Face) (e : (LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.ControlledAdaptiveComplex.L✝ K U hU f hf phi hphi).Edge) (het : ↑e ⊆ (LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.ControlledAdaptiveComplex.L✝ K U hU f hf phi hphi).faceVertices t) {eps : ℝ} (heps : 0 < eps) (hepsDist : ∀ (p q : ↑U), p ∈ (LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.ControlledAdaptiveComplex.L✝ K U hU f hf phi hphi).faceCarrier t → q ∈ (LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.ControlledAdaptiveComplex.L✝ K U hU f hf phi hphi).faceCarrier t → dist (f p) (f q) ≤ eps / 4) : Metric.diam (G.edgeImage e) ≤ eps / 4

Every edge belonging to a controlled adaptive face has image diameter bounded by that face's selected scale.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.ControlledAdaptiveComplex.exists_faceBoundary_control (K : IntrinsicTwoComplex) (U : Set K.realization) (hU : IsOpen U) (f : ↑U → Plane) (hf : Continuous f) (phi : ↑U → ℝ) (hphi : StronglyPositiveOn Set.univ phi) (G : (LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.ControlledAdaptiveComplex.L✝ K U hU f hf phi hphi).PlaneGraphRealization) (hmap : ∀ (p : ↑(LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.ControlledAdaptiveComplex.L✝ K U hU f hf phi hphi).support), G.map p = f ↑p) (t : (LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.ControlledAdaptiveComplex.L✝ K U hU f hf phi hphi).Face) (p : ↑(LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.ControlledAdaptiveComplex.L✝ K U hU f hf phi hphi).support) (hp : p ∈ LocallyFiniteTriangleComplex.PlaneGraphRealization.faceInSupport t) (q : LocallyFiniteTriangleComplex.StandardFaceBoundary) : ∃ (eps : ℝ), 0 < eps ∧ eps ≤ 1 ∧ dist (G.graphReplacementMap (LocallyFiniteTriangleComplex.faceBoundaryLift t q)) (G.map ↑(LocallyFiniteTriangleComplex.faceBoundaryLift t q)) + dist (G.map ↑(LocallyFiniteTriangleComplex.faceBoundaryLift t q)) (G.map p) ≤ eps ∧ eps ≤ phi ↑p

The boundary error on one adaptive face is bounded by a positive scale which is at most both the prescribed pointwise tolerance and one.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.ControlledAdaptiveComplex.faceBoundariesControlled (K : IntrinsicTwoComplex) (U : Set K.realization) (hU : IsOpen U) (f : ↑U → Plane) (hf : Continuous f) (phi : ↑U → ℝ) (hphi : StronglyPositiveOn Set.univ phi) (G : (LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.ControlledAdaptiveComplex.L✝ K U hU f hf phi hphi).PlaneGraphRealization) (hmap : ∀ (p : ↑(LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.ControlledAdaptiveComplex.L✝ K U hU f hf phi hphi).support), G.map p = f ↑p) : LocallyFiniteTriangleComplex.FaceBoundariesControlled G fun (p : ↑(LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.ControlledAdaptiveComplex.L✝ K U hU f hf phi hphi).support) => phi ↑p

The adaptive mesh discharges the exact face-boundary estimate consumed by the cellwise Schoenflies extension.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.ControlledAdaptiveComplex.range_graphReplacementMap_subset_halfPlane (K : IntrinsicTwoComplex) (U : Set K.realization) (hU : IsOpen U) (f : ↑U → Plane) (hf : Continuous f) (phi : ↑U → ℝ) (hphi : StronglyPositiveOn Set.univ phi) (G : (LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.ControlledAdaptiveComplex.L✝ K U hU f hf phi hphi).PlaneGraphRealization) (hmap : ∀ (p : ↑(LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.ControlledAdaptiveComplex.L✝ K U hU f hf phi hphi).support), G.map p = f ↑p) (hfHalf : Set.range f ⊆ HalfPlaneSet) : Set.range G.graphReplacementMap ⊆ HalfPlaneSet

If the original controlled realization lies in the model half-plane, so does its entire simultaneous polygonal replacement graph.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.RegionControlledAdaptiveComplex.faceBoundariesControlled (K : IntrinsicTwoComplex) (U : Set K.realization) (hU : IsOpen U) (V : Set Plane) (hV : IsOpen V) (f : ↑U → Plane) (hf : Continuous f) (hmem : ∀ (x : ↑U), f x ∈ V) (phi : ↑U → ℝ) (hphi : StronglyPositiveOn Set.univ phi) (G : (LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.RegionControlledAdaptiveComplex.R✝ K U hU V hV f hf hmem phi hphi).PlaneGraphRealization) (hmap : ∀ (p : ↑(LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.RegionControlledAdaptiveComplex.R✝ K U hU V hV f hf hmem phi hphi).support), G.map p = f ↑p) : LocallyFiniteTriangleComplex.FaceBoundariesControlled G fun (p : ↑(LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.RegionControlledAdaptiveComplex.R✝ K U hU V hV f hf hmem phi hphi).support) => regionSafeControl V f phi ↑p

The adaptive face-boundary estimate for the frontier-reduced tolerance.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.RegionControlledAdaptiveComplex.uniformFrontierControl (K : IntrinsicTwoComplex) (U : Set K.realization) (hU : IsOpen U) (V : Set Plane) (hV : IsOpen V) (f : ↑U → Plane) (hf : Continuous f) (hmem : ∀ (x : ↑U), f x ∈ V) (phi : ↑U → ℝ) (hphi : StronglyPositiveOn Set.univ phi) (G : (LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.RegionControlledAdaptiveComplex.R✝ K U hU V hV f hf hmem phi hphi).PlaneGraphRealization) (hmap : ∀ (p : ↑(LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.RegionControlledAdaptiveComplex.R✝ K U hU V hV f hf hmem phi hphi).support), G.map p = f ↑p) (hregion : G.region = V) : G.UniformFrontierControl fun (p : ↑(LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.RegionControlledAdaptiveComplex.R✝ K U hU V hV f hf hmem phi hphi).support) => regionSafeControl V f phi ↑p

The tolerance consumed by the filling is uniformly bounded and frontier-relative.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.RegionControlledAdaptiveComplex.closedRegions_mem_region (K : IntrinsicTwoComplex) (U : Set K.realization) (hU : IsOpen U) (V : Set Plane) (hV : IsOpen V) (f : ↑U → Plane) (hf : Continuous f) (hmem : ∀ (x : ↑U), f x ∈ V) (phi : ↑U → ℝ) (hphi : StronglyPositiveOn Set.univ phi) (G : (LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.RegionControlledAdaptiveComplex.R✝ K U hU V hV f hf hmem phi hphi).PlaneGraphRealization) (hmap : ∀ (p : ↑(LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.RegionControlledAdaptiveComplex.R✝ K U hU V hV f hf hmem phi hphi).support), G.map p = f ↑p) (hregion : G.region = V) (t : (LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.RegionControlledAdaptiveComplex.R✝ K U hU V hV f hf hmem phi hphi).Face) : (LocallyFiniteTriangleComplex.facePolygonalCircle t).closedRegion ⊆ G.region

The frontier-reduced adaptive fillings lie in the open target region.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.RegionControlledAdaptiveComplex.locallyFinite_closedRegions (K : IntrinsicTwoComplex) (U : Set K.realization) (hU : IsOpen U) (V : Set Plane) (hV : IsOpen V) (f : ↑U → Plane) (hf : Continuous f) (hmem : ∀ (x : ↑U), f x ∈ V) (phi : ↑U → ℝ) (hphi : StronglyPositiveOn Set.univ phi) (G : (LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.RegionControlledAdaptiveComplex.R✝ K U hU V hV f hf hmem phi hphi).PlaneGraphRealization) (hmap : ∀ (p : ↑(LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.RegionControlledAdaptiveComplex.R✝ K U hU V hV f hf hmem phi hphi).support), G.map p = f ↑p) (hregion : G.region = V) : LocallyFinite fun (t : (LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.RegionControlledAdaptiveComplex.R✝ K U hU V hV f hf hmem phi hphi).Face) => {q : ↑G.region | ↑q ∈ (LocallyFiniteTriangleComplex.facePolygonalCircle t).closedRegion}

The frontier-reduced adaptive fillings form a locally finite family in the open target.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.RegionControlledAdaptiveComplex.faceVertices_injective (K : IntrinsicTwoComplex) (U : Set K.realization) (hU : IsOpen U) (V : Set Plane) (hV : IsOpen V) (f : ↑U → Plane) (hf : Continuous f) (hmem : ∀ (x : ↑U), f x ∈ V) (phi : ↑U → ℝ) (hphi : StronglyPositiveOn Set.univ phi) : Function.Injective (LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.RegionControlledAdaptiveComplex.R✝ K U hU V hV f hf hmem phi hphi).faceVertices

The region-controlled adaptive complex carries distinct vertex triples on distinct faces: the hfaces entry condition of exists_polygonalReplacement holds unconditionally.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.RegionControlledAdaptiveComplex.exists_polygonalReplacement (K : IntrinsicTwoComplex) (U : Set K.realization) (hU : IsOpen U) (V : Set Plane) (hV : IsOpen V) (f : ↑U → Plane) (hf : Continuous f) (hmem : ∀ (x : ↑U), f x ∈ V) (phi : ↑U → ℝ) (hphi : StronglyPositiveOn Set.univ phi) (G : (LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.RegionControlledAdaptiveComplex.R✝ K U hU V hV f hf hmem phi hphi).PlaneGraphRealization) (hmap : ∀ (p : ↑(LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.RegionControlledAdaptiveComplex.R✝ K U hU V hV f hf hmem phi hphi).support), G.map p = f ↑p) (hregion : G.region = V) (hfaces : Function.Injective (LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.RegionControlledAdaptiveComplex.R✝ K U hU V hV f hf hmem phi hphi).faceVertices) (hsep : LocallyFiniteTriangleComplex.SeparatesVerticesFromFaces G fun (p : ↑(LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.RegionControlledAdaptiveComplex.R✝ K U hU V hV f hf hmem phi hphi).support) => regionSafeControl V f phi ↑p) : ∃ (H : LocallyFiniteTriangleComplex.CellwiseCompatibility G), ∀ (p : ↑(LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.RegionControlledAdaptiveComplex.R✝ K U hU V hV f hf hmem phi hphi).support), dist (↑↑((LocallyFiniteTriangleComplex.polygonalReplacementHomeomorph H) p)) (G.map p) ≤ phi ↑p

Complete locally finite cellwise replacement once the remaining side-separation condition is supplied. Region containment and local finiteness are now consequences, not hypotheses.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.RegionControlledAdaptiveComplex.exists_polygonalReplacement_of_comparison (K : IntrinsicTwoComplex) (U : Set K.realization) (hU : IsOpen U) (V : Set Plane) (hV : IsOpen V) (f : ↑U → Plane) (hf : Continuous f) (hmem : ∀ (x : ↑U), f x ∈ V) (phi : ↑U → ℝ) (hphi : StronglyPositiveOn Set.univ phi) (G : (LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.RegionControlledAdaptiveComplex.R✝ K U hU V hV f hf hmem phi hphi).PlaneGraphRealization) (hmap : ∀ (p : ↑(LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.RegionControlledAdaptiveComplex.R✝ K U hU V hV f hf hmem phi hphi).support), G.map p = f ↑p) (hregion : G.region = V) : ∃ (vc : (LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.RegionControlledAdaptiveComplex.R✝ K U hU V hV f hf hmem phi hphi).Vertex → ℝ) (hvc : ∀ (v : (LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.RegionControlledAdaptiveComplex.R✝ K U hU V hV f hf hmem phi hphi).Vertex), 0 < vc v) (ec : (LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.RegionControlledAdaptiveComplex.R✝ K U hU V hV f hf hmem phi hphi).Edge → ℝ) (hec : ∀ (e : (LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.RegionControlledAdaptiveComplex.R✝ K U hU V hV f hf hmem phi hphi).Edge), 0 < ec e) (H : LocallyFiniteTriangleComplex.CellwiseCompatibility (G.withApproximationControls vc hvc ec hec)), ∀ (p : ↑(LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.RegionControlledAdaptiveComplex.R✝ K U hU V hV f hf hmem phi hphi).support), dist (↑↑((LocallyFiniteTriangleComplex.polygonalReplacementHomeomorph H) p)) (G.map p) ≤ phi ↑p

Complete locally finite cellwise replacement with no residual side hypothesis. The separation entry of exists_polygonalReplacement is discharged by the facewise comparison map after shrinking the arc approximation controls; the shrunken realization keeps the map, the region, and the frontier-reduced tolerance, so all adaptive control theorems reapply.