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

theorem inner_shapeOperator_eq_hessian_div_gradNorm {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) (hx : x ∈ patch.domain) (ψ : (Fin (n + 1) → ℝ) → ℝ) (hψ_ne_zero : fderiv ℝ ψ (patch.f x) ≠ 0) (hψ_smooth : ContDiffAt ℝ 2 ψ (patch.f x)) (himage : ∀ u ∈ patch.domain, ψ (patch.f u) = 0) : ∃ (s : ℝ) (_ : s = 1 ∨ s = -1), ∀ (i j : Fin n), shapeOperator patch x i j = s * ((firstFundamentalForm patch x)⁻¹ * Matrix.of fun (a b : Fin n) => ((fderiv ℝ (fderiv ℝ ψ) (patch.f x)) (patch.partialDeriv x a)) (patch.partialDeriv x b) / ‖fderiv ℝ ψ (patch.f x)‖) i j

theorem normalCurvature_denom_pos {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) (hx : x ∈ patch.domain) (X : Fin n → ℝ) (hX : X ≠ 0) : 0 < X ⬝ᵥ (firstFundamentalForm patch x).mulVec X

theorem normalCurvature_eq_ratio {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) (hx : x ∈ patch.domain) (X : Fin n → ℝ) : normalCurvature patch x X = X ⬝ᵥ (firstFundamentalForm patch x).mulVec ((shapeOperator patch x).mulVec X) / X ⬝ᵥ (firstFundamentalForm patch x).mulVec X