structure CombinatorialGaussBonnet.CompactCombinatorialSurface : Type 1

• numPolygons : ℕ
• polygon : Fin self.numPolygons → Set (Fin 3 → ℝ)
• polygon_convex (i : Fin self.numPolygons) : Convex ℝ (self.polygon i)
• polygon_flat (i : Fin self.numPolygons) : ∃ (p : Fin 3 → ℝ) (n : Fin 3 → ℝ), n ≠ 0 ∧ ∀ x ∈ self.polygon i, ∑ k : Fin 3, (x k - p k) * n k = 0
• Vertex : Type
• finVertex : Fintype self.Vertex
• vertexPos : self.Vertex → Fin 3 → ℝ
• Edge : Type
• finEdge : Fintype self.Edge
• decEdge : DecidableEq self.Edge
• edgeSet : self.Edge → Set (Fin 3 → ℝ)
• edgesOf : Fin self.numPolygons → Finset self.Edge
• edge_subset (i : Fin self.numPolygons) (e : self.Edge) : e ∈ self.edgesOf i → self.edgeSet e ⊆ self.polygon i
• disjoint_or_common_edge (i j : Fin self.numPolygons) : i ≠ j → Disjoint (self.polygon i) (self.polygon j) ∨ ∃ e ∈ self.edgesOf i, e ∈ self.edgesOf j
• edge_exactly_two (i : Fin self.numPolygons) (e : self.Edge) : e ∈ self.edgesOf i → ∃! j : Fin self.numPolygons, j ≠ i ∧ e ∈ self.edgesOf j

noncomputable def CombinatorialGaussBonnet.CompactCombinatorialSurface.numVertices (S : CompactCombinatorialSurface) : ℕ

noncomputable def CombinatorialGaussBonnet.CompactCombinatorialSurface.numEdges (S : CompactCombinatorialSurface) : ℕ

noncomputable def CombinatorialGaussBonnet.CompactCombinatorialSurface.eulerCharacteristic (S : CompactCombinatorialSurface) : ℤ

structure CombinatorialGaussBonnet.SurfaceTriangulation : Type 1

• V : Type
• E : Type
• F : Type
• finV : Fintype self.V
• finE : Fintype self.E
• finF : Fintype self.F
• decV : DecidableEq self.V
• decF : DecidableEq self.F
• facesAt : self.V → Finset self.F
• angleAt : self.V → self.F → ℝ
• verticesOf : self.F → Finset self.V
• face_card (f : self.F) : (self.verticesOf f).card = 3
• mem_facesAt_iff (v : self.V) (f : self.F) : f ∈ self.facesAt v ↔ v ∈ self.verticesOf f
• angle_sum_face (f : self.F) : ∑ v ∈ self.verticesOf f, self.angleAt v f = Real.pi
• two_edges_eq_three_faces : 2 * Fintype.card self.E = 3 * Fintype.card self.F

noncomputable def CombinatorialGaussBonnet.SurfaceTriangulation.numVertices (T : SurfaceTriangulation) : ℕ

noncomputable def CombinatorialGaussBonnet.SurfaceTriangulation.numEdges (T : SurfaceTriangulation) : ℕ

noncomputable def CombinatorialGaussBonnet.SurfaceTriangulation.numFaces (T : SurfaceTriangulation) : ℕ

noncomputable def CombinatorialGaussBonnet.SurfaceTriangulation.eulerCharacteristic (T : SurfaceTriangulation) : ℤ

noncomputable def CombinatorialGaussBonnet.SurfaceTriangulation.gaussCurvatureComb (T : SurfaceTriangulation) (v : T.V) : ℝ

theorem CombinatorialGaussBonnet.combinatorial_gauss_bonnet (T : SurfaceTriangulation) : Finset.univ.sum T.gaussCurvatureComb = 2 * Real.pi * ↑T.eulerCharacteristic

structure SmoothGaussBonnet.Triangulation (M : Set (Fin 3 → ℝ)) : Type 1

• Vertex : Type
• finVertex : Fintype self.Vertex
• decVertex : DecidableEq self.Vertex
• Edge : Type
• finEdge : Fintype self.Edge
• decEdge : DecidableEq self.Edge
• Face : Type
• finFace : Fintype self.Face
• decFace : DecidableEq self.Face
• vertexPos : self.Vertex → Fin 3 → ℝ
• vertex_mem (v : self.Vertex) : self.vertexPos v ∈ M
• faceRegion : self.Face → Set (Fin 3 → ℝ)
• face_subset (f : self.Face) : self.faceRegion f ⊆ M
• covering (p : Fin 3 → ℝ) : p ∈ M → ∃ (f : self.Face), p ∈ self.faceRegion f
• faceVertices : self.Face → Fin 3 → self.Vertex
• faceVertices_injective (f : self.Face) : Function.Injective (self.faceVertices f)
• edgeEndpoints : self.Edge → Fin 2 → self.Vertex
• edgeEndpoints_injective (e : self.Edge) : Function.Injective (self.edgeEndpoints e)
• faceEdges : self.Face → Fin 3 → self.Edge
• edge_shared_by_two (e : self.Edge) : ∃ (f₁ : self.Face) (f₂ : self.Face), f₁ ≠ f₂ ∧ ∀ (f : self.Face), e ∈ Set.range (self.faceEdges f) → f = f₁ ∨ f = f₂
• intersection_regularity (f₁ f₂ : self.Face) : f₁ ≠ f₂ → self.faceRegion f₁ ∩ self.faceRegion f₂ = ∅ ∨ (∃ (v : self.Vertex), self.faceRegion f₁ ∩ self.faceRegion f₂ = {self.vertexPos v}) ∨ ∃ e ∈ Set.range (self.faceEdges f₁), e ∈ Set.range (self.faceEdges f₂)

noncomputable def SmoothGaussBonnet.Triangulation.numVertices {M : Set (Fin 3 → ℝ)} (τ : Triangulation M) : ℕ

noncomputable def SmoothGaussBonnet.Triangulation.numEdges {M : Set (Fin 3 → ℝ)} (τ : Triangulation M) : ℕ

noncomputable def SmoothGaussBonnet.Triangulation.numFaces {M : Set (Fin 3 → ℝ)} (τ : Triangulation M) : ℕ

noncomputable def SmoothGaussBonnet.Triangulation.eulerCharacteristic {M : Set (Fin 3 → ℝ)} (τ : Triangulation M) : ℤ

structure SmoothGaussBonnet.MovingFrameWithSingularities (M : Set (EuclideanSpace ℝ (Fin 3))) : Type

• singularPoints : Finset (EuclideanSpace ℝ (Fin 3))
• sing_in_M (p : EuclideanSpace ℝ (Fin 3)) : p ∈ self.singularPoints → p ∈ M
• frame₁ : ↑(M \ ↑self.singularPoints) → EuclideanSpace ℝ (Fin 3)
• frame₂ : ↑(M \ ↑self.singularPoints) → EuclideanSpace ℝ (Fin 3)
• surfaceNormal : ↑(M \ ↑self.singularPoints) → EuclideanSpace ℝ (Fin 3)
• frame₁_unit (y : ↑(M \ ↑self.singularPoints)) : ‖self.frame₁ y‖ = 1
• frame₂_unit (y : ↑(M \ ↑self.singularPoints)) : ‖self.frame₂ y‖ = 1
• normal_unit (y : ↑(M \ ↑self.singularPoints)) : ‖self.surfaceNormal y‖ = 1
• frame_orthogonal (y : ↑(M \ ↑self.singularPoints)) : inner ℝ (self.frame₁ y) (self.frame₂ y) = 0
• frame₁_tangent (y : ↑(M \ ↑self.singularPoints)) : inner ℝ (self.frame₁ y) (self.surfaceNormal y) = 0
• frame₂_tangent (y : ↑(M \ ↑self.singularPoints)) : inner ℝ (self.frame₂ y) (self.surfaceNormal y) = 0
• frame_pos_oriented (y : ↑(M \ ↑self.singularPoints)) : 0 < (Matrix.of fun (i j : Fin 3) => (![self.frame₁ y, self.frame₂ y, self.surfaceNormal y] j).ofLp i).det
• multiplicity : ↥self.singularPoints → ℤ

structure SmoothGaussBonnet.CompactSurface : Type 1

• carrier : Set (Fin 3 → ℝ)
• carrier_smooth : GaussMapDegree.IsSmHypersurface 2 self.carrier
• carrier_compact : IsCompact self.carrier
• carrier_nonempty : self.carrier.Nonempty
• gaussMap : (Fin 3 → ℝ) → Fin 3 → ℝ
• gaussMap_maps_to_sphere (p : Fin 3 → ℝ) : p ∈ self.carrier → ‖self.gaussMap p‖ = 1
• gaussianCurvature : (Fin 3 → ℝ) → ℝ
• localParam : (Fin 2 → ℝ) → Fin 3 → ℝ
• localParamInv : (Fin 3 → ℝ) → Fin 2 → ℝ
• gaussianCurvature_eq (p : Fin 3 → ℝ) : p ∈ self.carrier → self.gaussianCurvature p = GaussMapDegree.jacobianDetAtPoint self.gaussMap self.localParam (self.localParamInv p) (self.gaussMap p)
• gaussMapDegree : ℤ
• gaussMapDegree_eq : ∫ (p : Fin 3 → ℝ) in self.carrier, self.gaussianCurvature p ∂MeasureTheory.Measure.hausdorffMeasure 2 = ↑self.gaussMapDegree * (4 * Real.pi)
• triangulation : CombinatorialGaussBonnet.SurfaceTriangulation
• vertexPos : self.triangulation.V → Fin 3 → ℝ
• vertices_in_carrier (v : self.triangulation.V) : self.vertexPos v ∈ self.carrier

noncomputable def SmoothGaussBonnet.CompactSurface.eulerCharacteristic (M : CompactSurface) : ℤ

noncomputable def SmoothGaussBonnet.CompactSurface.totalGaussianCurvature (M : CompactSurface) : ℝ

theorem SmoothGaussBonnet.totalGaussianCurvature_eq_degree (M : CompactSurface) : M.totalGaussianCurvature = ↑M.gaussMapDegree * (4 * Real.pi)

theorem SmoothGaussBonnet.totalGaussianCurvature_eq_degree_general {n : ℕ} (f : GaussMapDegree.SmoothMapToSphere n) : (-1) ^ n * ∫ (p : Fin (n + 1) → ℝ) in f.M, f.tangentMapDet p ∂MeasureTheory.Measure.hausdorffMeasure ↑n = (-1) ^ n * GaussMapDegree.sphereVolume n * ↑(GaussMapDegree.degreeOfMap f)

theorem SmoothGaussBonnet.totalCurvature_eq_combinatorial (M : CompactSurface) : M.totalGaussianCurvature = Finset.univ.sum M.triangulation.gaussCurvatureComb

theorem SmoothGaussBonnet.eulerCharacteristic_eq (M : CompactSurface) : M.eulerCharacteristic = M.triangulation.eulerCharacteristic

theorem SmoothGaussBonnet.smooth_gauss_bonnet (M : CompactSurface) : M.totalGaussianCurvature = 2 * Real.pi * ↑M.eulerCharacteristic

theorem SmoothGaussBonnet.euler_characteristic_eq_twice_degree (M : CompactSurface) : M.eulerCharacteristic = 2 * M.gaussMapDegree

structure CompactSurfaceCurvature.CompactSurface : Type

• M : Set (Fin 3 → ℝ)
• M_compact : IsCompact self.M
• M_connected : IsConnected self.M
• M_nonempty : self.M.Nonempty
• gaussMap : (Fin 3 → ℝ) → Fin 3 → ℝ
• gaussMap_smooth : ContDiffOn ℝ ⊤ self.gaussMap self.M
• gaussMap_maps_to_sphere (p : Fin 3 → ℝ) : p ∈ self.M → ‖self.gaussMap p‖ = 1
• gaussianCurvature : (Fin 3 → ℝ) → ℝ
• localParam : (Fin 2 → ℝ) → Fin 3 → ℝ
• localParamInv : (Fin 3 → ℝ) → Fin 2 → ℝ
• gaussianCurvature_eq (p : Fin 3 → ℝ) : p ∈ self.M → self.gaussianCurvature p = GaussMapDegree.jacobianDetAtPoint self.gaussMap self.localParam (self.localParamInv p) (self.gaussMap p)
• gaussMapDegree : ℤ
• gaussMap_degree_ge_one : 1 ≤ |self.gaussMapDegree|

noncomputable def CompactSurfaceCurvature.CompactSurface.totalAbsCurvature (S : CompactSurface) : ℝ

theorem CompactSurfaceCurvature.totalAbsCurvature_ge_degree_times_sphere_area (S : CompactSurface) : S.totalAbsCurvature ≥ ↑|S.gaussMapDegree| * (4 * Real.pi)

theorem CompactSurfaceCurvature.total_abs_curvature_ge_four_pi (S : CompactSurface) : S.totalAbsCurvature ≥ 4 * Real.pi

structure GaussBonnetBoundary.DiscRegion : Type

• surface : Set (Fin 3 → ℝ)
• region : Set (Fin 3 → ℝ)
• region_subset : self.region ⊆ self.surface
• region_connected : IsPathConnected self.region
• numCorners : ℕ
• gaussianCurvature : (Fin 3 → ℝ) → ℝ
• patch : HypersurfacePatch 2
• paramDomain : Set (Fin 2 → ℝ)
• paramDomain_sub : self.paramDomain ⊆ self.patch.domain
• region_eq : self.region = self.patch.f '' self.paramDomain
• curvature_consistent (x : Fin 2 → ℝ) : x ∈ self.paramDomain → self.gaussianCurvature (self.patch.f x) = gaussCurvature self.patch x
• totalGaussianCurvature : ℝ
• totalCurvature_eq : self.totalGaussianCurvature = ∫ (x : Fin 2 → ℝ) in self.paramDomain, gaussCurvature self.patch x * √(firstFundamentalForm self.patch x).det
• totalGeodesicCurvature : ℝ
• exteriorAngles : Fin self.numCorners → ℝ

noncomputable def GaussBonnetBoundary.DiscRegion.sumExteriorAngles (D : DiscRegion) : ℝ

theorem GaussBonnetBoundary.gauss_bonnet_with_boundary (D : DiscRegion) : D.totalGaussianCurvature + D.totalGeodesicCurvature + D.sumExteriorAngles = 2 * Real.pi

structure GaussBonnetBoundary.GeodesicTriangleRegionextends GaussBonnetBoundary.DiscRegion : Type

• surface : Set (Fin 3 → ℝ)
• region : Set (Fin 3 → ℝ)
• region_subset : self.region ⊆ self.surface
• region_connected : IsPathConnected self.region
• numCorners : ℕ
• gaussianCurvature : (Fin 3 → ℝ) → ℝ
• patch : HypersurfacePatch 2
• paramDomain : Set (Fin 2 → ℝ)
• paramDomain_sub : self.paramDomain ⊆ self.patch.domain
• region_eq : self.region = self.patch.f '' self.paramDomain
• curvature_consistent (x : Fin 2 → ℝ) : x ∈ self.paramDomain → self.gaussianCurvature (self.patch.f x) = gaussCurvature self.patch x
• totalGaussianCurvature : ℝ
• totalCurvature_eq : self.totalGaussianCurvature = ∫ (x : Fin 2 → ℝ) in self.paramDomain, gaussCurvature self.patch x * √(firstFundamentalForm self.patch x).det
• totalGeodesicCurvature : ℝ
• exteriorAngles : Fin self.numCorners → ℝ
• corners_eq : self.numCorners = 3
• angle₁ : ℝ
• angle₂ : ℝ
• angle₃ : ℝ
• geodesic_boundary : self.totalGeodesicCurvature = 0
• ext_angle_0 : self.exteriorAngles (Fin.cast ⋯ 0) = Real.pi - self.angle₁
• ext_angle_1 : self.exteriorAngles (Fin.cast ⋯ 1) = Real.pi - self.angle₂
• ext_angle_2 : self.exteriorAngles (Fin.cast ⋯ 2) = Real.pi - self.angle₃

theorem GaussBonnetBoundary.GeodesicTriangleRegion.sum_exterior_eq (Δ : GeodesicTriangleRegion) : Δ.sumExteriorAngles = 3 * Real.pi - (Δ.angle₁ + Δ.angle₂ + Δ.angle₃)

theorem GaussBonnetBoundary.geodesic_triangle_angle_sum (Δ : GeodesicTriangleRegion) : Δ.angle₁ + Δ.angle₂ + Δ.angle₃ = Real.pi + Δ.totalGaussianCurvature