noncomputable def MovingFrame.firstFundamentalFormBilinear (patch : HypersurfacePatch 2) (x v w : Fin 2 → ℝ) : ℝ

noncomputable def MovingFrame.geodesicCurvature (patch : HypersurfacePatch 2) (c : ℝ → Fin 2 → ℝ) (t : ℝ) : ℝ

theorem MovingFrame.geodesicCurvature_eq_connection_formula (patch : HypersurfacePatch 2) (X : (Fin 2 → ℝ) → Matrix (Fin 2) (Fin 2) ℝ) (c : ℝ → Fin 2 → ℝ) (hF : IsMovingFrame patch X) (hpos : ∀ x ∈ patch.domain, 0 < (X x).det) (hsmooth : ContDiff ℝ ⊤ c) (hdom : ∀ (t : ℝ), c t ∈ patch.domain) (hspeed : ∀ (t : ℝ), firstFundamentalFormBilinear patch (c t) (deriv c t) (deriv c t) > 0) (hX1 : ∀ (t : ℝ) (k : Fin 2), X (c t) k 0 = deriv c t k / √(firstFundamentalFormBilinear patch (c t) (deriv c t) (deriv c t))) (t : ℝ) : geodesicCurvature patch c t = (connectionMatrix patch X (c t) 0 0 1 * deriv c t 0 + connectionMatrix patch X (c t) 1 0 1 * deriv c t 1) / √(firstFundamentalFormBilinear patch (c t) (deriv c t) (deriv c t))