def Minkowski.minkowskiInner (n : ℕ) (v w : Fin (n + 1) → ℝ) : ℝ

def Minkowski.IsPositiveDefiniteOn {n : ℕ} (S : Submodule ℝ (Fin (n + 1) → ℝ)) : Prop

noncomputable def Minkowski.partials {n : ℕ} (f : (Fin n → ℝ) → Fin (n + 1) → ℝ) (x : Fin n → ℝ) : Fin n → Fin (n + 1) → ℝ

structure Minkowski.SpacelikeHypersurface (n : ℕ) : Type

• U : Set (Fin n → ℝ)
• hU : IsOpen self.U
• f : (Fin n → ℝ) → Fin (n + 1) → ℝ
• smooth : ContDiffOn ℝ ⊤ self.f self.U
• linearIndep (x : Fin n → ℝ) : x ∈ self.U → LinearIndependent ℝ (partials self.f x)
• spacelike (x : Fin n → ℝ) : x ∈ self.U → IsPositiveDefiniteOn (Submodule.span ℝ (Set.range (partials self.f x)))

noncomputable def Minkowski.orientationMatrix {n : ℕ} (f : (Fin n → ℝ) → Fin (n + 1) → ℝ) (x : Fin n → ℝ) (ν : Fin (n + 1) → ℝ) : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ

structure Minkowski.IsGaussNormal {n : ℕ} (S : SpacelikeHypersurface n) (x : Fin n → ℝ) (ν : Fin (n + 1) → ℝ) : Prop

• timelike : minkowskiInner n ν ν = -1
• orthogonal (i : Fin n) : minkowskiInner n ν (partials S.f x i) = 0
• positive_orientation : (orientationMatrix S.f x ν).det > 0

theorem Minkowski.minkowskiInner_smul_self {n : ℕ} (c : ℝ) (v : Fin (n + 1) → ℝ) : minkowskiInner n (c • v) (c • v) = c ^ 2 * minkowskiInner n v v

theorem Minkowski.minkowskiInner_smul_left {n : ℕ} (c : ℝ) (v w : Fin (n + 1) → ℝ) : minkowskiInner n (c • v) w = c * minkowskiInner n v w

theorem Minkowski.minkowski_orthogonal_complement_positive_definite {n : ℕ} (X : Fin (n + 1) → ℝ) (hX : minkowskiInner n X X < 0) (Y : Fin (n + 1) → ℝ) : Y ≠ 0 → minkowskiInner n X Y = 0 → minkowskiInner n Y Y > 0