noncomputable def GaussMapDegree.gramMatrix (n : ℕ) (σ : (Fin n → ℝ) → Fin (n + 1) → ℝ) (u : Fin n → ℝ) : Matrix (Fin n) (Fin n) ℝ

def GaussMapDegree.augmentedMatrix {n : ℕ} (B : Matrix (Fin (n + 1)) (Fin n) ℝ) (ν : Fin (n + 1) → ℝ) : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ

structure GaussMapDegree.SmoothHypersurfaceMap (n : ℕ) : Type

• domainU : Set (Fin n → ℝ)
• domainU_open : IsOpen self.domainU
• domainV : Set (Fin n → ℝ)
• domainV_open : IsOpen self.domainV
• σ : (Fin n → ℝ) → Fin (n + 1) → ℝ
• τ : (Fin n → ℝ) → Fin (n + 1) → ℝ
• σ_smooth : ContDiffOn ℝ ⊤ self.σ self.domainU
• σ_immersion (u : Fin n → ℝ) : u ∈ self.domainU → Function.Injective ⇑(fderiv ℝ self.σ u)
• τ_smooth : ContDiffOn ℝ ⊤ self.τ self.domainV
• τ_immersion (v : Fin n → ℝ) : v ∈ self.domainV → Function.Injective ⇑(fderiv ℝ self.τ v)
• h : (Fin n → ℝ) → Fin n → ℝ
• h_maps (u : Fin n → ℝ) : u ∈ self.domainU → self.h u ∈ self.domainV
• h_smooth : ContDiffOn ℝ ⊤ self.h self.domainU
• chain_rule (u : Fin n → ℝ) : u ∈ self.domainU → ((Matrix.of fun (i : Fin (n + 1)) (j : Fin n) => (fderiv ℝ self.σ u) (Function.update 0 j 1) i) * Matrix.of fun (i j : Fin n) => (fderiv ℝ self.h u) (Function.update 0 j 1) i) = Matrix.of fun (i : Fin (n + 1)) (j : Fin n) => (fderiv ℝ (self.τ ∘ self.h) u) (Function.update 0 j 1) i
• ν : (Fin n → ℝ) → Fin (n + 1) → ℝ
• ν_tilde : (Fin n → ℝ) → Fin (n + 1) → ℝ
• ν_orth (u : Fin n → ℝ) : u ∈ self.domainU → ∀ (j : Fin n), ∑ i : Fin (n + 1), (fderiv ℝ self.σ u) (Function.update 0 j 1) i * self.ν u i = 0
• ν_norm (u : Fin n → ℝ) : u ∈ self.domainU → ∑ i : Fin (n + 1), self.ν u i ^ 2 = 1
• ν_tilde_orth (v : Fin n → ℝ) : v ∈ self.domainV → ∀ (j : Fin n), ∑ i : Fin (n + 1), (fderiv ℝ self.τ v) (Function.update 0 j 1) i * self.ν_tilde v i = 0
• ν_tilde_norm (v : Fin n → ℝ) : v ∈ self.domainV → ∑ i : Fin (n + 1), self.ν_tilde v i ^ 2 = 1
• σ_pos_oriented (u : Fin n → ℝ) : u ∈ self.domainU → 0 < (augmentedMatrix (fun (i : Fin (n + 1)) (j : Fin n) => (fderiv ℝ self.σ u) (Function.update 0 j 1) i) (self.ν u)).det
• τ_pos_oriented (v : Fin n → ℝ) : v ∈ self.domainV → 0 < (augmentedMatrix (fun (i : Fin (n + 1)) (j : Fin n) => (fderiv ℝ self.τ v) (Function.update 0 j 1) i) (self.ν_tilde v)).det

noncomputable def GaussMapDegree.SmoothHypersurfaceMap.jacobianMatrix {n : ℕ} (Φ : SmoothHypersurfaceMap n) (u : Fin n → ℝ) : Matrix (Fin n) (Fin n) ℝ

noncomputable def GaussMapDegree.SmoothHypersurfaceMap.jacobianDet {n : ℕ} (Φ : SmoothHypersurfaceMap n) (u : Fin n → ℝ) : ℝ

theorem GaussMapDegree.det_augmented_eq_det_mul {n : ℕ} (H : Matrix (Fin n) (Fin n) ℝ) (A : Matrix (Fin (n + 1)) (Fin n) ℝ) (ν : Fin (n + 1) → ℝ) : (augmentedMatrix (A * H) ν).det = H.det * (augmentedMatrix A ν).det

theorem GaussMapDegree.det_jacobian_formula {n : ℕ} (Df Dφf : Matrix (Fin (n + 1)) (Fin n) ℝ) (ν_tilde : Fin (n + 1) → ℝ) (H : Matrix (Fin n) (Fin n) ℝ) (hchain : Df * H = Dφf) (hG_pos : 0 < (augmentedMatrix Df ν_tilde).det) (hG_sq : (augmentedMatrix Df ν_tilde).det ^ 2 = (Df.transpose * Df).det) : H.det = (augmentedMatrix Dφf ν_tilde).det / √(Df.transpose * Df).det

noncomputable def GaussMapDegree.SmoothHypersurfaceMap.sourceJacobian {n : ℕ} (Φ : SmoothHypersurfaceMap n) (u : Fin n → ℝ) : Matrix (Fin (n + 1)) (Fin n) ℝ

noncomputable def GaussMapDegree.SmoothHypersurfaceMap.composedJacobian {n : ℕ} (Φ : SmoothHypersurfaceMap n) (u : Fin n → ℝ) : Matrix (Fin (n + 1)) (Fin n) ℝ

theorem GaussMapDegree.SmoothHypersurfaceMap.chain_rule_matrices {n : ℕ} (Φ : SmoothHypersurfaceMap n) (u : Fin n → ℝ) (hu : u ∈ Φ.domainU) : Φ.sourceJacobian u * Φ.jacobianMatrix u = Φ.composedJacobian u

theorem GaussMapDegree.det_augmented_sq_of_orthonormal_last_col {n : ℕ} (A : Matrix (Fin (n + 1)) (Fin n) ℝ) (ν : Fin (n + 1) → ℝ) (horth : ∀ (j : Fin n), ∑ i : Fin (n + 1), A i j * ν i = 0) (hnorm : ∑ i : Fin (n + 1), ν i ^ 2 = 1) : (augmentedMatrix A ν).det ^ 2 = (A.transpose * A).det

theorem GaussMapDegree.det_jacobian_formula_geometric {n : ℕ} (Φ : SmoothHypersurfaceMap n) (u : Fin n → ℝ) (ν_tilde : Fin (n + 1) → ℝ) (horth : ∀ (j : Fin n), ∑ i : Fin (n + 1), Φ.sourceJacobian u i j * ν_tilde i = 0) (hnorm : ∑ i : Fin (n + 1), ν_tilde i ^ 2 = 1) (hpos : 0 < (augmentedMatrix (Φ.sourceJacobian u) ν_tilde).det) (hchain : Φ.sourceJacobian u * Φ.jacobianMatrix u = Φ.composedJacobian u) : Φ.jacobianDet u = (augmentedMatrix (Φ.composedJacobian u) ν_tilde).det / √(gramMatrix n Φ.σ u).det

theorem GaussMapDegree.det_jacobian_formula_geometric_target {n : ℕ} (Φ : SmoothHypersurfaceMap n) (u : Fin n → ℝ) (htarget_orth_source : ∀ (j : Fin n), ∑ i : Fin (n + 1), Φ.sourceJacobian u i j * Φ.ν_tilde (Φ.h u) i = 0) (hpos : 0 < (augmentedMatrix (Φ.sourceJacobian u) (Φ.ν_tilde (Φ.h u))).det) (hu : u ∈ Φ.domainU) : Φ.jacobianDet u = (augmentedMatrix (Φ.composedJacobian u) (Φ.ν_tilde (Φ.h u))).det / √(gramMatrix n Φ.σ u).det

def GaussMapDegree.IsSmHypersurface (n : ℕ) (M : Set (Fin (n + 1) → ℝ)) : Prop

structure GaussMapDegree.SmoothMapBetweenHypersurfaces (n : ℕ) : Type

• φ : (Fin (n + 1) → ℝ) → Fin (n + 1) → ℝ
• φ_smooth : ContDiff ℝ ⊤ self.φ
• M : Set (Fin (n + 1) → ℝ)
• M_compact : IsCompact self.M
• M_hypersurface : IsSmHypersurface n self.M
• M_oriented : ∃ (ν : (Fin (n + 1) → ℝ) → Fin (n + 1) → ℝ), Continuous ν ∧ ∀ p ∈ self.M, ‖ν p‖ = 1
• M_tilde : Set (Fin (n + 1) → ℝ)
• M_tilde_compact : IsCompact self.M_tilde
• M_tilde_connected : IsConnected self.M_tilde
• M_tilde_hypersurface : IsSmHypersurface n self.M_tilde
• M_tilde_oriented : ∃ (ν : (Fin (n + 1) → ℝ) → Fin (n + 1) → ℝ), Continuous ν ∧ ∀ p ∈ self.M_tilde, ‖ν p‖ = 1
• φ_maps_to_target (p : Fin (n + 1) → ℝ) : p ∈ self.M → self.φ p ∈ self.M_tilde

noncomputable def GaussMapDegree.hypersurfaceVolume (n : ℕ) (S : Set (Fin (n + 1) → ℝ)) : ℝ

structure GaussMapDegree.SmoothMapToSphere (n : ℕ) : Type

• φ : (Fin (n + 1) → ℝ) → Fin (n + 1) → ℝ
• φ_smooth : ContDiff ℝ ⊤ self.φ
• M : Set (Fin (n + 1) → ℝ)
• M_compact : IsCompact self.M
• M_hypersurface : IsSmHypersurface n self.M
• M_oriented : ∃ (ν : (Fin (n + 1) → ℝ) → Fin (n + 1) → ℝ), Continuous ν ∧ ∀ p ∈ self.M, ‖ν p‖ = 1
• φ_maps_to_sphere (p : Fin (n + 1) → ℝ) : p ∈ self.M → ‖self.φ p‖ = 1

noncomputable def GaussMapDegree.sphereVolume (n : ℕ) : ℝ

noncomputable def GaussMapDegree.jacobianDetAtPoint {n : ℕ} (φ : (Fin (n + 1) → ℝ) → Fin (n + 1) → ℝ) (σ : (Fin n → ℝ) → Fin (n + 1) → ℝ) (u : Fin n → ℝ) (ν_tilde : Fin (n + 1) → ℝ) : ℝ

noncomputable def GaussMapDegree.SmoothMapBetweenHypersurfaces.tangentMapDet {n : ℕ} (f : SmoothMapBetweenHypersurfaces n) (p : Fin (n + 1) → ℝ) : ℝ

noncomputable def GaussMapDegree.degreeOfMapBetweenHypersurfacesReal {n : ℕ} (f : SmoothMapBetweenHypersurfaces n) : ℝ

noncomputable def GaussMapDegree.degreeOfMapBetweenHypersurfaces {n : ℕ} (f : SmoothMapBetweenHypersurfaces n) : ℤ

def GaussMapDegree.SmoothMapToSphere.toSmoothMapBetweenHypersurfaces {n : ℕ} (f : SmoothMapToSphere n) (sphere_hypersurface : IsSmHypersurface n {x : Fin (n + 1) → ℝ | ‖x‖ = 1}) (sphere_connected : IsConnected {x : Fin (n + 1) → ℝ | ‖x‖ = 1}) (sphere_compact : IsCompact {x : Fin (n + 1) → ℝ | ‖x‖ = 1}) (sphere_oriented : ∃ (ν : (Fin (n + 1) → ℝ) → Fin (n + 1) → ℝ), Continuous ν ∧ ∀ p ∈ {x : Fin (n + 1) → ℝ | ‖x‖ = 1}, ‖ν p‖ = 1) : SmoothMapBetweenHypersurfaces n

noncomputable def GaussMapDegree.SmoothMapToSphere.tangentMapDet {n : ℕ} (f : SmoothMapToSphere n) (p : Fin (n + 1) → ℝ) : ℝ

noncomputable def GaussMapDegree.degreeOfMapReal {n : ℕ} (f : SmoothMapToSphere n) : ℝ

noncomputable def GaussMapDegree.degreeOfMap {n : ℕ} (f : SmoothMapToSphere n) : ℤ

theorem GaussMapDegree.degree_zero_of_image_avoids_point {n : ℕ} (f : SmoothMapToSphere n) (q : Fin (n + 1) → ℝ) (hq : ‖q‖ = 1) (himage : ∀ p ∈ f.M, f.φ p ≠ q) : degreeOfMap f = 0

theorem GaussMapDegree.degree_eq_zero_of_not_surjective {n : ℕ} (f : SmoothMapToSphere n) (h : ∃ (q : Fin (n + 1) → ℝ), ‖q‖ = 1 ∧ ∀ p ∈ f.M, f.φ p ≠ q) : degreeOfMap f = 0

theorem GaussMapDegree.surjective_of_degree_ne_zero {n : ℕ} (f : SmoothMapToSphere n) (hdeg : degreeOfMap f ≠ 0) (q : Fin (n + 1) → ℝ) : ‖q‖ = 1 → ∃ p ∈ f.M, f.φ p = q

theorem GaussMapDegree.area_formula_bijective_pos_det {n : ℕ} (f : SmoothMapBetweenHypersurfaces n) (hbij : Function.Bijective fun (p : ↑f.M) => f.φ ↑p) (hdet_pos : ∀ p ∈ f.M, 0 < f.tangentMapDet p) : ∫ (p : Fin (n + 1) → ℝ) in f.M, f.tangentMapDet p ∂MeasureTheory.Measure.hausdorffMeasure ↑n = hypersurfaceVolume n f.M_tilde

theorem GaussMapDegree.degree_of_bijective_pos_det {n : ℕ} (f : SmoothMapBetweenHypersurfaces n) (hbij : Function.Bijective fun (p : ↑f.M) => f.φ ↑p) (hdet_pos : ∀ p ∈ f.M, 0 < f.tangentMapDet p) (hvol_pos : 0 < hypersurfaceVolume n f.M_tilde) : degreeOfMapBetweenHypersurfaces f = 1