structure HypersurfacePatch (n : ℕ) : Type

• domain : Set (Fin n → ℝ)
• domain_open : IsOpen self.domain
• f : (Fin n → ℝ) → Fin (n + 1) → ℝ
• smooth : ContDiffOn ℝ ⊤ self.f self.domain
• immersion (x : Fin n → ℝ) : x ∈ self.domain → Function.Injective ⇑(fderiv ℝ self.f x)

noncomputable def HypersurfacePatch.partialDeriv {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) (i : Fin n) : Fin (n + 1) → ℝ

def generalizedCross {n : ℕ} (v : Fin n → Fin (n + 1) → ℝ) : Fin (n + 1) → ℝ

noncomputable def orientationMatrix {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) (w : Fin (n + 1) → ℝ) : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ

noncomputable def gaussNormal {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) : Fin (n + 1) → ℝ

noncomputable def firstFundamentalForm {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) : Matrix (Fin n) (Fin n) ℝ

noncomputable def jacobianMatrix {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) : Matrix (Fin (n + 1)) (Fin n) ℝ

theorem firstFundamentalForm_eq_conjTranspose_mul {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) : firstFundamentalForm patch x = (jacobianMatrix patch x).conjTranspose * jacobianMatrix patch x

theorem jacobian_mulVec_eq_fderiv {n : ℕ} (patch : HypersurfacePatch n) (x v : Fin n → ℝ) : (jacobianMatrix patch x).mulVec v = (fderiv ℝ patch.f x) v

theorem firstFundamentalForm_posDef {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) (hx : x ∈ patch.domain) : (firstFundamentalForm patch x).PosDef

theorem gaussNormal_unit {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) (hx : x ∈ patch.domain) : √(gaussNormal patch x ⬝ᵥ gaussNormal patch x) = 1

theorem gaussNormal_orthogonal {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) (hx : x ∈ patch.domain) (i : Fin n) : gaussNormal patch x ⬝ᵥ patch.partialDeriv x i = 0

theorem gaussNormal_orientation {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) (hx : x ∈ patch.domain) : (orientationMatrix patch x (gaussNormal patch x)).det > 0

noncomputable def secondFundamentalForm {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) : Matrix (Fin n) (Fin n) ℝ

theorem secondFundamentalForm_symmetric {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) (hx : x ∈ patch.domain) (i j : Fin n) : secondFundamentalForm patch x i j = secondFundamentalForm patch x j i

noncomputable def shapeOperator {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) : Matrix (Fin n) (Fin n) ℝ

def IsPrincipalCurvature {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) (κ : ℝ) : Prop

theorem dotProduct_sum_smul {m k : ℕ} (v : Fin k → Fin m → ℝ) (a : Fin k → ℝ) (w : Fin m → ℝ) : (∑ j : Fin k, a j • v j) ⬝ᵥ w = ∑ j : Fin k, a j * v j ⬝ᵥ w

theorem gaussNormal_deriv_in_tangent {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) (hx : x ∈ patch.domain) (i : Fin n) : ∃ (a : Fin n → ℝ), (fderiv ℝ (gaussNormal patch) x) (Pi.single i 1) = ∑ j : Fin n, a j • (fderiv ℝ patch.f x) (Pi.single j 1)

theorem gaussNormal_deriv_dot_partial {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) (hx : x ∈ patch.domain) (i j : Fin n) : (fderiv ℝ (gaussNormal patch) x) (Pi.single i 1) ⬝ᵥ (fderiv ℝ patch.f x) (Pi.single j 1) = -secondFundamentalForm patch x i j

theorem gauss_normal_derivative {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) (hx : x ∈ patch.domain) (i : Fin n) : (fderiv ℝ (gaussNormal patch) x) (Pi.single i 1) = -∑ j : Fin n, shapeOperator patch x j i • (fderiv ℝ patch.f x) (Pi.single j 1)

noncomputable def meanCurvature {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) : ℝ

noncomputable def gaussCurvature {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) : ℝ

noncomputable def scalarCurvature {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) : ℝ

theorem rigidity_theorem {n : ℕ} (patch₁ patch₂ : HypersurfacePatch n) (hconn : IsConnected patch₁.domain) (hdomain : patch₁.domain = patch₂.domain) (hG : ∀ x ∈ patch₁.domain, firstFundamentalForm patch₁ x = firstFundamentalForm patch₂ x) (hH : ∀ x ∈ patch₁.domain, secondFundamentalForm patch₁ x = secondFundamentalForm patch₂ x) : ∃ (A : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ) (b : Fin (n + 1) → ℝ), A ∈ Matrix.orthogonalGroup (Fin (n + 1)) ℝ ∧ A.det = 1 ∧ ∀ x ∈ patch₁.domain, patch₂.f x = A.mulVec (patch₁.f x) + b

noncomputable def coordinateJacobian {n : ℕ} (φ : (Fin n → ℝ) → Fin n → ℝ) (x : Fin n → ℝ) : Matrix (Fin n) (Fin n) ℝ

theorem generalizedCross_linear_combination {n : ℕ} (v : Fin n → Fin (n + 1) → ℝ) (A : Matrix (Fin n) (Fin n) ℝ) : (generalizedCross fun (i : Fin n) => ∑ j : Fin n, A j i • v j) = A.det • generalizedCross v

theorem gaussNormal_coordinate_change {n : ℕ} (patch tildeP : HypersurfacePatch n) (φ : (Fin n → ℝ) → Fin n → ℝ) (x : Fin n → ℝ) (h_eq : tildeP.f = patch.f ∘ φ) (hφ : DifferentiableAt ℝ φ x) (hf : DifferentiableAt ℝ patch.f (φ x)) (hdet_pos : (coordinateJacobian φ x).det > 0) : gaussNormal tildeP x = gaussNormal patch (φ x)

theorem firstFundamentalForm_coordinate_change {n : ℕ} (patch tildeP : HypersurfacePatch n) (φ : (Fin n → ℝ) → Fin n → ℝ) (x : Fin n → ℝ) (h_eq : tildeP.f = patch.f ∘ φ) (hφ : DifferentiableAt ℝ φ x) (hf : DifferentiableAt ℝ patch.f (φ x)) : firstFundamentalForm tildeP x = (coordinateJacobian φ x).transpose * firstFundamentalForm patch (φ x) * coordinateJacobian φ x

theorem secondFundamentalForm_coordinate_change_of_entries {n : ℕ} (patch tildeP : HypersurfacePatch n) (φ : (Fin n → ℝ) → Fin n → ℝ) (x : Fin n → ℝ) (h_chain : ∀ (i j : Fin n), secondFundamentalForm tildeP x i j = ∑ k : Fin n, ∑ l : Fin n, coordinateJacobian φ x k i * secondFundamentalForm patch (φ x) k l * coordinateJacobian φ x l j) : secondFundamentalForm tildeP x = (coordinateJacobian φ x).transpose * secondFundamentalForm patch (φ x) * coordinateJacobian φ x

theorem secondFundamentalForm_entry_formula {n : ℕ} (patch tildeP : HypersurfacePatch n) (φ : (Fin n → ℝ) → Fin n → ℝ) (x : Fin n → ℝ) (h_eq : tildeP.f = patch.f ∘ φ) (hφ_smooth : ContDiffAt ℝ ⊤ φ x) (hf_smooth : ContDiffAt ℝ ⊤ patch.f (φ x)) (hx : x ∈ tildeP.domain) (hφx : φ x ∈ patch.domain) (hdet_pos : (coordinateJacobian φ x).det > 0) (i j : Fin n) : secondFundamentalForm tildeP x i j = ∑ k : Fin n, ∑ l : Fin n, coordinateJacobian φ x k i * secondFundamentalForm patch (φ x) k l * coordinateJacobian φ x l j

theorem secondFundamentalForm_coordinate_change {n : ℕ} (patch tildeP : HypersurfacePatch n) (φ : (Fin n → ℝ) → Fin n → ℝ) (x : Fin n → ℝ) (h_eq : tildeP.f = patch.f ∘ φ) (hφ_smooth : ContDiffAt ℝ ⊤ φ x) (hf_smooth : ContDiffAt ℝ ⊤ patch.f (φ x)) (hx : x ∈ tildeP.domain) (hφx : φ x ∈ patch.domain) (hdet_pos : (coordinateJacobian φ x).det > 0) : secondFundamentalForm tildeP x = (coordinateJacobian φ x).transpose * secondFundamentalForm patch (φ x) * coordinateJacobian φ x

theorem shapeOperator_coordinate_change {n : ℕ} (patch tildeP : HypersurfacePatch n) (φ : (Fin n → ℝ) → Fin n → ℝ) (x : Fin n → ℝ) (hG : firstFundamentalForm tildeP x = (coordinateJacobian φ x).transpose * firstFundamentalForm patch (φ x) * coordinateJacobian φ x) (hH : secondFundamentalForm tildeP x = (coordinateJacobian φ x).transpose * secondFundamentalForm patch (φ x) * coordinateJacobian φ x) (hφ_det : IsUnit (coordinateJacobian φ x).det) (hG_det : IsUnit (firstFundamentalForm patch (φ x)).det) : shapeOperator tildeP x = (coordinateJacobian φ x)⁻¹ * shapeOperator patch (φ x) * coordinateJacobian φ x

theorem prop_13_1 {n : ℕ} (patch tildeP : HypersurfacePatch n) (φ : (Fin n → ℝ) → Fin n → ℝ) (x : Fin n → ℝ) (h_eq : tildeP.f = patch.f ∘ φ) (hφ_smooth : ContDiffAt ℝ ⊤ φ x) (hf_smooth : ContDiffAt ℝ ⊤ patch.f (φ x)) (hx : x ∈ tildeP.domain) (hφx : φ x ∈ patch.domain) (hdet_pos : (coordinateJacobian φ x).det > 0) (hG_det : IsUnit (firstFundamentalForm patch (φ x)).det) : gaussNormal tildeP x = gaussNormal patch (φ x) ∧ firstFundamentalForm tildeP x = (coordinateJacobian φ x).transpose * firstFundamentalForm patch (φ x) * coordinateJacobian φ x ∧ secondFundamentalForm tildeP x = (coordinateJacobian φ x).transpose * secondFundamentalForm patch (φ x) * coordinateJacobian φ x ∧ shapeOperator tildeP x = (coordinateJacobian φ x)⁻¹ * shapeOperator patch (φ x) * coordinateJacobian φ x

noncomputable def normalDerivMatrix {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ

theorem firstFundamentalForm_eq_transpose_mul {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) : firstFundamentalForm patch x = (jacobianMatrix patch x).transpose * jacobianMatrix patch x

theorem shape_operator_parametrization_identification {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) (hx : x ∈ patch.domain) (X : Fin n → ℝ) : (jacobianMatrix patch x).mulVec ((shapeOperator patch x).mulVec X) = -(fderiv ℝ (gaussNormal patch) x) X

theorem firstFundamentalForm_eq_transpose_mul_and_shapeOperator_intertwine {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) (hx : x ∈ patch.domain) : firstFundamentalForm patch x = (jacobianMatrix patch x).transpose * jacobianMatrix patch x ∧ ∀ (X : Fin n → ℝ), (jacobianMatrix patch x).mulVec ((shapeOperator patch x).mulVec X) = -(fderiv ℝ (gaussNormal patch) x) X

theorem dotProduct_self_eq_one_of_sqrt_eq_one {n : ℕ} (ν : Fin (n + 1) → ℝ) (h : √(ν ⬝ᵥ ν) = 1) : ν ⬝ᵥ ν = 1

theorem orientationMatrix_transpose_mul_block {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) (hx : x ∈ patch.domain) : ((orientationMatrix patch x (gaussNormal patch x)).transpose * orientationMatrix patch x (gaussNormal patch x)).submatrix ⇑finSumFinEquiv ⇑finSumFinEquiv = Matrix.fromBlocks (firstFundamentalForm patch x) 0 0 1

theorem orientationMatrix_det_eq_sqrt_det_G {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) (hx : x ∈ patch.domain) : (orientationMatrix patch x (gaussNormal patch x)).det = √(firstFundamentalForm patch x).det

theorem det_gram_eq_cross_dotProduct_self (v : Fin 2 → Fin 3 → ℝ) : (Matrix.of fun (i j : Fin 2) => v i ⬝ᵥ v j).det = generalizedCross v ⬝ᵥ generalizedCross v

noncomputable def shapeOperatorLinkingMatrix {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ

theorem shapeOperatorLinkingMatrix_det {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) : (shapeOperatorLinkingMatrix patch x).det = (-1) ^ n * (shapeOperator patch x).det

theorem normalDerivMatrix_eq_mul {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) (hx : x ∈ patch.domain) : normalDerivMatrix patch x = orientationMatrix patch x (gaussNormal patch x) * shapeOperatorLinkingMatrix patch x

theorem gaussCurvature_normal_formula {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) (hx : x ∈ patch.domain) : gaussCurvature patch x = (-1) ^ n * (normalDerivMatrix patch x).det / √(firstFundamentalForm patch x).det

def IsCompactHypersurface {n : ℕ} (M : Set (EuclideanSpace ℝ (Fin (n + 1)))) : Prop