Affine standard-coordinate formulas for adaptive fan faces

The adaptive fan realization is assembled through faithful midpoint subdivisions. Although its definition is geometric, on each named fan triangle its value in the original intrinsic barycentric coordinates is one affine function of the standard planar face coordinates. The relative Radó weld uses this formula after composing with the inverse-affine pieces of retained polygonal filling certificates.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceCoordExtensionAffineLF {S : Type u_1} [TopologicalSpace S] (L : LocallyFiniteTriangleComplex S) (f : L.Face) : (Fin 3 → ℝ) →ᵃ[ℝ] ↥(L.faceVertices f) → ℝ

Reindex standard coordinates onto the literal three-vertex type of one locally finite face.

Equations

• L.faceCoordExtensionAffineLF f = AffineMap.pi fun (v : ↥(L.faceVertices f)) => (LinearMap.proj ((L.faceVertexEquiv f).symm v)).toAffineMap

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceCoordExtensionAffineLF_apply {S : Type u_1} [TopologicalSpace S] (L : LocallyFiniteTriangleComplex S) (f : L.Face) (z : Fin 3 → ℝ) (v : ↥(L.faceVertices f)) : (L.faceCoordExtensionAffineLF f) z v = z ((L.faceVertexEquiv f).symm v)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.facePlaneInverseAffineLF {S : Type u_1} [TopologicalSpace S] (L : LocallyFiniteTriangleComplex S) (f : L.Face) : Plane →ᵃ[ℝ] ↥(L.faceVertices f) → ℝ

The affine inverse-coordinate formula for the standard plane chart of a locally finite face.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.facePlaneHomeomorph_symm_val_LF {S : Type u_1} [TopologicalSpace S] (L : LocallyFiniteTriangleComplex S) (f : L.Face) (p : ↑standardTrianglePlaneComplex.support) : ↑((L.facePlaneHomeomorph f).symm p) = (L.facePlaneInverseAffineLF f) ↑p

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanRelabel_source_sum_apply {K : IntrinsicTwoComplex} {U : Set K.realization} [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) (x : ↑(stdSimplex ℝ ↥(K.adaptiveGlobalFanFaceVertices U hU f))) (v : (K.safeSubdivision f.fst.fst).refined.Vertex) : ∑ p : ↥(K.adaptiveFanFaceVertices U hU f), (K.adaptiveFanRelabelSimplex U hU f x) p * ↑(K.adaptiveFanVertexSource U hU f p) v = ∑ p : ↥(K.adaptiveFanFaceVertices U hU f), x ((K.adaptiveFanFaceVertexEquiv U hU f).symm p) * ↑(K.adaptiveFanVertexSource U hU f p) v

Relabeling a global adaptive fan simplex preserves the source-weighted affine sum.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveGlobalFanFaceMap_standardAffine_point {K : IntrinsicTwoComplex} {U : Set K.realization} [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) (aQ : ((K.safeSubdivision f.fst.fst).refined.Vertex → ℝ) →ᵃ[ℝ] K.Vertex → ℝ) (haQ : ∀ z ∈ (K.safeSubdivision f.fst.fst).refined.faceCarrier ↑↑f.fst.snd, ↑((K.safeSubdivision f.fst.fst).homeo z) = aQ ↑z) (b : (↥(K.adaptiveGlobalFanFaceVertices U hU f) → ℝ) →ₗ[ℝ] (K.safeSubdivision f.fst.fst).refined.Vertex → ℝ) (hb : ∀ (z : ↥(K.adaptiveGlobalFanFaceVertices U hU f) → ℝ) (v : (K.safeSubdivision f.fst.fst).refined.Vertex), b z v = ∑ p : ↥(K.adaptiveFanFaceVertices U hU f), z ((K.adaptiveFanFaceVertexEquiv U hU f).symm p) * ↑(K.adaptiveFanVertexSource U hU f p) v) (x : ↑(stdSimplex ℝ ↥(K.adaptiveGlobalFanFaceVertices U hU f))) : ↑((K.safeSubdivision f.fst.fst).homeo (K.adaptiveFanSourcePoint U hU f (K.adaptiveFanRelabelSimplex U hU f x))) = aQ (b (((K.adaptiveLocallyFiniteTriangleComplex U hU).facePlaneInverseAffineLF f) ↑(((K.adaptiveLocallyFiniteTriangleComplex U hU).facePlaneHomeomorph f) x)))

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveGlobalFanAffinePiece {K : IntrinsicTwoComplex} {U : Set K.realization} [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) : ((K.safeSubdivision f.fst.fst).refined.Vertex → ℝ) →ᵃ[ℝ] K.Vertex → ℝ

The affine subdivision map on the refined face supporting a global fan.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveGlobalFanAffinePiece hU f = Classical.choose ⋯

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveGlobalFanLinearPiece {K : IntrinsicTwoComplex} {U : Set K.realization} [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) : (↥(K.adaptiveGlobalFanFaceVertices U hU f) → ℝ) →ₗ[ℝ] (K.safeSubdivision f.fst.fst).refined.Vertex → ℝ

The linear map that relabels global fan coordinates into refined coordinates.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveGlobalFanMapStandardAffine {K : IntrinsicTwoComplex} {U : Set K.realization} [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) : Plane →ᵃ[ℝ] K.Vertex → ℝ

The affine map describing one global adaptive fan face in standard coordinates.

Equations

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

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveGlobalFanSimplex {K : IntrinsicTwoComplex} {U : Set K.realization} [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) : Set (↥(K.adaptiveGlobalFanFaceVertices U hU f) → ℝ)

The standard simplex indexing a global adaptive fan face.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveGlobalFanSimplex hU f = stdSimplex ℝ ↥(K.adaptiveGlobalFanFaceVertices U hU f)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveGlobalFanFaceMapValue {K : IntrinsicTwoComplex} {U : Set K.realization} [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) : ↑(adaptiveGlobalFanSimplex hU f) → K.Vertex → ℝ

The intrinsic-coordinate value of a global adaptive fan face map.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveGlobalFanFaceMapValue hU f x = ↑↑(K.adaptiveGlobalFanFaceMap U hU f x)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveGlobalFanMapStandardAffine_apply {K : IntrinsicTwoComplex} {U : Set K.realization} [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) (x : ↑(stdSimplex ℝ ↥(K.adaptiveGlobalFanFaceVertices U hU f))) : adaptiveGlobalFanFaceMapValue hU f x = (adaptiveGlobalFanMapStandardAffine hU f) ↑(((K.adaptiveLocallyFiniteTriangleComplex U hU).facePlaneHomeomorph f) x)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveGlobalFanFaceMap_standardAffine {K : IntrinsicTwoComplex} {U : Set K.realization} [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) : ∃ (a : Plane →ᵃ[ℝ] K.Vertex → ℝ), ∀ (x : ↑(adaptiveGlobalFanSimplex hU f)), adaptiveGlobalFanFaceMapValue hU f x = a ↑(((K.adaptiveLocallyFiniteTriangleComplex U hU).facePlaneHomeomorph f) x)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanFaceMap_val_eq_vertex_sum {K : IntrinsicTwoComplex} {U : Set K.realization} [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) (x : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU f))) : ↑↑(K.adaptiveFanFaceMap U hU f x) = fun (v : K.Vertex) => ∑ p : ↥(K.adaptiveFanFaceVertices U hU f), x p * ↑↑p v

On one local fan triangle, the transported old barycentric coordinates are the barycentric weighted sum of the coordinates of its three geometric vertices. This is the supporting-face formula used by the bordered chart straightening.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveGlobalFanFaceMap_val_eq_vertex_sum {K : IntrinsicTwoComplex} {U : Set K.realization} [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) (x : ↑(stdSimplex ℝ ↥(K.adaptiveGlobalFanFaceVertices U hU f))) : ↑↑(K.adaptiveGlobalFanFaceMap U hU f x) = fun (k : K.Vertex) => ∑ v : ↥(K.adaptiveGlobalFanFaceVertices U hU f), x v * ↑↑↑v k

The same vertex-sum formula after relabeling a fan triangle by the global vertex type of the locally finite adaptive complex.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveGlobalFanFaceVerticesInCarrier {K : IntrinsicTwoComplex} {U : Set K.realization} [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) (b : Finset K.Vertex) : Finset (K.AdaptiveFanVertex U hU)

The vertices of an adaptive fan face whose geometric source points lie in an old barycentric carrier.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveGlobalFanFaceVerticesInCarrier hU f b = {w ∈ K.adaptiveGlobalFanFaceVertices U hU f | ↑w ∈ K.faceCarrier b}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveGlobalFanFaceMap_mem_faceCarrier_iff_supported {K : IntrinsicTwoComplex} {U : Set K.realization} [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) (b : Finset K.Vertex) (x : ↑(stdSimplex ℝ ↥(K.adaptiveGlobalFanFaceVertices U hU f))) : ↑(K.adaptiveGlobalFanFaceMap U hU f x) ∈ K.faceCarrier b ↔ ∀ (v : ↥(K.adaptiveGlobalFanFaceVertices U hU f)), ↑v ∉ adaptiveGlobalFanFaceVerticesInCarrier hU f b → x v = 0

Pulling an old barycentric face carrier back to one adaptive fan triangle gives the simplex face spanned by precisely those adaptive vertices which lie in the old carrier.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFaceCenter_not_mem_faceCarrier_of_subordinate {K : IntrinsicTwoComplex} {U : Set K.realization} [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) (t : K.Face) (hsub : ∀ x ∈ (K.safeSubdivision f.fst.fst).refined.faceCarrier ↑↑f.fst.snd, (K.safeSubdivision f.fst.fst).homeo x ∈ K.faceCarrier ↑t) (b : Finset K.Vertex) (hbt : b ⊆ ↑t) (hbcard : b.card ≤ 2) : K.adaptiveFaceCenter U f.fst ∉ K.faceCarrier b

The cone center of an adaptive fan face lies in the relative interior of its unique level-zero parent. Hence it misses every proper old face of cardinality at most two in any old triangle to which the refined face is subordinate.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveGlobalFanFaceMap_exists_exposedFace {K : IntrinsicTwoComplex} {U : Set K.realization} [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) (b : Finset K.Vertex) (v₀ : ↥(K.adaptiveGlobalFanFaceVertices U hU f)) (hv₀ : ↑↑v₀ ∉ K.faceCarrier b) : ∃ d ⊆ K.adaptiveGlobalFanFaceVertices U hU f, d.card ≤ 2 ∧ ∀ (x : ↑(stdSimplex ℝ ↥(K.adaptiveGlobalFanFaceVertices U hU f))), ↑(K.adaptiveGlobalFanFaceMap U hU f x) ∈ K.faceCarrier b ↔ ∀ (v : ↥(K.adaptiveGlobalFanFaceVertices U hU f)), ↑v ∉ d → x v = 0

If one declared fan vertex misses an old carrier, that pullback carrier has at most two vertices and hence is an exposed proper face of the adaptive triangle.