theorem SpaceCurves.gram_schmidt_orthonormalization {n k : ℕ} (_hk : k ≤ n) (v : Fin k → EuclideanSpace ℝ (Fin n)) (hli : LinearIndependent ℝ v) : ∃ (e : Fin k → EuclideanSpace ℝ (Fin n)), Orthonormal ℝ e ∧ (∀ (i : Fin k), Submodule.span ℝ (Set.range fun (j : Fin (↑i + 1)) => e ⟨↑j, ⋯⟩) = Submodule.span ℝ (Set.range fun (j : Fin (↑i + 1)) => v ⟨↑j, ⋯⟩)) ∧ ∀ (i : Fin k), 0 < inner ℝ (e i) (v i)

theorem SpaceCurves.gram_schmidt_orthonormalization_unique {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {k : ℕ} (v e₁ e₂ : Fin k → E) (hon₁ : Orthonormal ℝ e₁) (hon₂ : Orthonormal ℝ e₂) (hspan₁ : ∀ (i : Fin k), Submodule.span ℝ (e₁ '' Set.Iic i) = Submodule.span ℝ (v '' Set.Iic i)) (hspan₂ : ∀ (i : Fin k), Submodule.span ℝ (e₂ '' Set.Iic i) = Submodule.span ℝ (v '' Set.Iic i)) (hpos₁ : ∀ (i : Fin k), 0 < inner ℝ (e₁ i) (v i)) (hpos₂ : ∀ (i : Fin k), 0 < inner ℝ (e₂ i) (v i)) : e₁ = e₂

theorem SpaceCurves.OrderedFinpartition.partSize_eq_one_of_length_eq {m : ℕ} (p : OrderedFinpartition m) (h : p.length = m) (i : Fin p.length) : p.partSize i = 1

theorem SpaceCurves.span_iteratedDeriv_comp_ge {n : ℕ} (c : ℝ → EuclideanSpace ℝ (Fin n)) (φ : ℝ → ℝ) (hc : ContDiff ℝ ⊤ c) (hφ : ContDiff ℝ ⊤ φ) (hφ' : ∀ (t : ℝ), 0 < deriv φ t) (t : ℝ) (j : ℕ) (hj : j < n - 1) : iteratedDeriv (j + 1) c (φ t) ∈ Submodule.span ℝ (Set.range fun (k : Fin (j + 1)) => iteratedDeriv (↑k + 1) (c ∘ φ) t)

theorem orthogonal_deriv_skew {n : ℕ} (E : ℝ → Matrix (Fin n) (Fin n) ℝ) (hE : ContDiff ℝ ⊤ E) (horth : ∀ (t : ℝ), E t ∈ Matrix.orthogonalGroup (Fin n) ℝ) (A : ℝ → Matrix (Fin n) (Fin n) ℝ) (hA : ∀ (t : ℝ), deriv E t = E t * A t) (t : ℝ) : (A t).transpose = -A t

def SpaceCurves.IsFrenetCurve {n : ℕ} (c : ℝ → EuclideanSpace ℝ (Fin n)) : Prop

noncomputable def SpaceCurves.frenetFrame {n : ℕ} (c : ℝ → EuclideanSpace ℝ (Fin n)) (_hc : IsFrenetCurve c) (t : ℝ) : Fin n → EuclideanSpace ℝ (Fin n)

noncomputable def SpaceCurves.frenetCurvature {n : ℕ} (c : ℝ → EuclideanSpace ℝ (Fin n)) (hc : IsFrenetCurve c) (i : Fin (n - 1)) (t : ℝ) : ℝ

noncomputable def SpaceCurves.frenetSerretMatrix {n : ℕ} (c : ℝ → EuclideanSpace ℝ (Fin n)) (hc : IsFrenetCurve c) (t : ℝ) : Matrix (Fin n) (Fin n) ℝ

theorem SpaceCurves.frenetFrame_differentiableAt {n : ℕ} (c : ℝ → EuclideanSpace ℝ (Fin n)) (hc : IsFrenetCurve c) (t : ℝ) (i : Fin n) : DifferentiableAt ℝ (fun (s : ℝ) => frenetFrame c hc s i) t

theorem SpaceCurves.frenetFrame_deriv_mem_span {n : ℕ} (c : ℝ → EuclideanSpace ℝ (Fin n)) (hc : IsFrenetCurve c) (t : ℝ) (j : Fin n) (hj : ↑j < n - 1) : deriv (fun (s : ℝ) => frenetFrame c hc s j) t ∈ Submodule.span ℝ (Set.range fun (i : Fin (↑j + 2)) => frenetFrame c hc t ⟨↑i, ⋯⟩)

theorem SpaceCurves.frenetFrame_inner_deriv_vanish {n : ℕ} (c : ℝ → EuclideanSpace ℝ (Fin n)) (hc : IsFrenetCurve c) (t : ℝ) (hn : 2 ≤ n) (hc' : ‖deriv c t‖ ≠ 0) (k j : Fin n) (h1 : ¬(↑j = ↑k + 1 ∧ ↑k < n - 1)) (h2 : ¬(↑k = ↑j + 1 ∧ ↑j < n - 1)) : inner ℝ (frenetFrame c hc t k) (deriv (fun (s : ℝ) => frenetFrame c hc s j) t) = 0

theorem SpaceCurves.frenetFrame_inner_deriv_super {n : ℕ} (c : ℝ → EuclideanSpace ℝ (Fin n)) (hc : IsFrenetCurve c) (t : ℝ) (hn : 2 ≤ n) (hc' : ‖deriv c t‖ ≠ 0) (k j : Fin n) (h : ↑j = ↑k + 1 ∧ ↑k < n - 1) : inner ℝ (frenetFrame c hc t k) (deriv (fun (s : ℝ) => frenetFrame c hc s j) t) = ‖deriv c t‖ * -frenetCurvature c hc ⟨↑k, ⋯⟩ t

theorem SpaceCurves.frenetFrame_inner_deriv_sub {n : ℕ} (c : ℝ → EuclideanSpace ℝ (Fin n)) (hc : IsFrenetCurve c) (t : ℝ) (hn : 2 ≤ n) (hc' : ‖deriv c t‖ ≠ 0) (k j : Fin n) (h1 : ¬(↑j = ↑k + 1 ∧ ↑k < n - 1)) (h : ↑k = ↑j + 1 ∧ ↑j < n - 1) : inner ℝ (frenetFrame c hc t k) (deriv (fun (s : ℝ) => frenetFrame c hc s j) t) = ‖deriv c t‖ * frenetCurvature c hc ⟨↑j, ⋯⟩ t

theorem SpaceCurves.frenetSerret_equation {n : ℕ} (c : ℝ → EuclideanSpace ℝ (Fin n)) (hc : IsFrenetCurve c) (t : ℝ) (hn : 2 ≤ n) (hc' : ‖deriv c t‖ ≠ 0) (j : Fin n) : deriv (fun (s : ℝ) => frenetFrame c hc s j) t = ‖deriv c t‖ • ∑ k : Fin n, frenetSerretMatrix c hc t k j • frenetFrame c hc t k

theorem SpaceCurves.frenetCurvature_eq_inner_div_norm {n : ℕ} (c : ℝ → EuclideanSpace ℝ (Fin n)) (hc : IsFrenetCurve c) (i : Fin (n - 1)) (t : ℝ) : frenetCurvature c hc i t = inner ℝ (frenetFrame c hc t ⟨↑i + 1, ⋯⟩) (deriv (fun (s : ℝ) => frenetFrame c hc s ⟨↑i, ⋯⟩) t) / ‖deriv c t‖

theorem SpaceCurves.frenetCurvature_pos {n : ℕ} (c : ℝ → EuclideanSpace ℝ (Fin n)) (hc : IsFrenetCurve c) (i : Fin (n - 1)) (hi : ↑i < n - 2) (t : ℝ) (hc' : ‖deriv c t‖ ≠ 0) : 0 < frenetCurvature c hc i t

theorem SpaceCurves.frenetSerret_theorem {n : ℕ} (c : ℝ → EuclideanSpace ℝ (Fin n)) (hc : IsFrenetCurve c) (t : ℝ) (hn : 2 ≤ n) (hc' : ‖deriv c t‖ ≠ 0) : (∀ (j : Fin n), deriv (fun (s : ℝ) => frenetFrame c hc s j) t = ‖deriv c t‖ • ∑ k : Fin n, frenetSerretMatrix c hc t k j • frenetFrame c hc t k) ∧ (∀ (i : Fin (n - 1)), ↑i < n - 2 → 0 < frenetCurvature c hc i t) ∧ ∀ (i : Fin (n - 1)), frenetCurvature c hc i t = inner ℝ (frenetFrame c hc t ⟨↑i + 1, ⋯⟩) (deriv (fun (s : ℝ) => frenetFrame c hc s ⟨↑i, ⋯⟩) t) / ‖deriv c t‖

theorem SpaceCurves.frenetFrame_orthogonal_higher_iteratedDeriv {n : ℕ} (c : ℝ → EuclideanSpace ℝ (Fin n)) (hc : IsFrenetCurve c) (s : ℝ) (i j : Fin n) (hij : ↑i < ↑j) (hi : ↑i < n - 1) : inner ℝ (frenetFrame c hc s j) (iteratedDeriv (↑i + 1) c s) = 0

theorem SpaceCurves.frenet_diagonal_entry_succ {n : ℕ} (c : ℝ → EuclideanSpace ℝ (Fin n)) (hc : IsFrenetCurve c) (t : ℝ) (hn : 2 ≤ n) (hc' : ‖deriv c t‖ ≠ 0) (i : Fin n) (hi : ↑i + 1 < n) : inner ℝ (frenetFrame c hc t ⟨↑i + 1, hi⟩) (iteratedDeriv (↑i + 2) c t) = ‖deriv c t‖ * frenetCurvature c hc ⟨↑i, ⋯⟩ t * inner ℝ (frenetFrame c hc t i) (iteratedDeriv (↑i + 1) c t)

theorem SpaceCurves.frenet_diagonal_entry_zero {n : ℕ} (c : ℝ → EuclideanSpace ℝ (Fin n)) (hc : IsFrenetCurve c) (t : ℝ) (hn : 2 ≤ n) (hc' : ‖deriv c t‖ ≠ 0) : inner ℝ (frenetFrame c hc t ⟨0, ⋯⟩) (iteratedDeriv 1 c t) = ‖deriv c t‖

theorem SpaceCurves.frenet_diagonal_entry {n : ℕ} (c : ℝ → EuclideanSpace ℝ (Fin n)) (hc : IsFrenetCurve c) (t : ℝ) (hn : 2 ≤ n) (hc' : ‖deriv c t‖ ≠ 0) (i : Fin n) : inner ℝ (frenetFrame c hc t i) (iteratedDeriv (↑i + 1) c t) = ‖deriv c t‖ ^ (↑i + 1) * ∏ k : Fin ↑i, frenetCurvature c hc ⟨↑k, ⋯⟩ t

theorem SpaceCurves.prod_fin_triangular {M : Type u_1} [CommMonoid M] (n : ℕ) (f : Fin (n - 1) → M) : ∏ i : Fin n, ∏ k : Fin ↑i, f ⟨↑k, ⋯⟩ = ∏ k : Fin (n - 1), f k ^ (n - 1 - ↑k)

theorem SpaceCurves.frenet_product_reindex {n : ℕ} (c : ℝ → EuclideanSpace ℝ (Fin n)) (hc : IsFrenetCurve c) (t : ℝ) (hn : 2 ≤ n) : ∏ i : Fin n, ∏ k : Fin ↑i, frenetCurvature c hc ⟨↑k, ⋯⟩ t = ∏ i : Fin (n - 1), frenetCurvature c hc i t ^ (n - 1 - ↑i)

theorem SpaceCurves.frenet_frame_det_one {n : ℕ} (c : ℝ → EuclideanSpace ℝ (Fin n)) (hc : IsFrenetCurve c) (t : ℝ) (hn : 2 ≤ n) (hc' : ‖deriv c t‖ ≠ 0) : (Matrix.of fun (k j : Fin n) => (frenetFrame c hc t k).ofLp j).det = 1

theorem SpaceCurves.frenet_det_factored {n : ℕ} (c : ℝ → EuclideanSpace ℝ (Fin n)) (hc : IsFrenetCurve c) (t : ℝ) (hn : 2 ≤ n) (hc' : ‖deriv c t‖ ≠ 0) : (Matrix.of fun (i j : Fin n) => (iteratedDeriv (↑i + 1) c t).ofLp j).det = ∏ i : Fin n, inner ℝ (frenetFrame c hc t i) (iteratedDeriv (↑i + 1) c t)

theorem SpaceCurves.frenet_det_formula {n : ℕ} (c : ℝ → EuclideanSpace ℝ (Fin n)) (hc : IsFrenetCurve c) (t : ℝ) (hn : 2 ≤ n) : (Matrix.of fun (i j : Fin n) => (iteratedDeriv (↑i + 1) c t).ofLp j).det / ‖deriv c t‖ ^ (n * (n + 1) / 2) = ∏ i : Fin (n - 1), frenetCurvature c hc i t ^ (n - 1 - ↑i)

theorem SpaceCurves.linearIndependent_of_span_eq {V : Type u_1} [AddCommGroup V] [Module ℝ V] {k : ℕ} (v w : Fin k → V) (hv : LinearIndependent ℝ v) (heq : Submodule.span ℝ (Set.range w) = Submodule.span ℝ (Set.range v)) : LinearIndependent ℝ w

theorem SpaceCurves.frenet_reparametrization_isFrenet {n : ℕ} (c : ℝ → EuclideanSpace ℝ (Fin n)) (φ : ℝ → ℝ) (hc : IsFrenetCurve c) (hφ : ContDiff ℝ ⊤ φ) (hφ' : ∀ (t : ℝ), 0 < deriv φ t) : IsFrenetCurve (c ∘ φ)

theorem SpaceCurves.frenetFrame_span_eq {n : ℕ} (c : ℝ → EuclideanSpace ℝ (Fin n)) (hc : IsFrenetCurve c) (t : ℝ) (i : Fin (n - 1)) : Submodule.span ℝ ((fun (j : Fin (n - 1)) => frenetFrame c hc t ⟨↑j, ⋯⟩) '' Set.Iic i) = Submodule.span ℝ ((fun (j : Fin (n - 1)) => iteratedDeriv (↑j + 1) c t) '' Set.Iic i)

theorem SpaceCurves.frenetFrame_inner_pos {n : ℕ} (c : ℝ → EuclideanSpace ℝ (Fin n)) (hc : IsFrenetCurve c) (t : ℝ) (i : Fin (n - 1)) : 0 < inner ℝ (frenetFrame c hc t ⟨↑i, ⋯⟩) (iteratedDeriv (↑i + 1) c t)

theorem SpaceCurves.span_iteratedDeriv_comp_eq_Iic {n : ℕ} (c : ℝ → EuclideanSpace ℝ (Fin n)) (φ : ℝ → ℝ) (hc : ContDiff ℝ ⊤ c) (hφ : ContDiff ℝ ⊤ φ) (hφ' : ∀ (t : ℝ), 0 < deriv φ t) (t : ℝ) (i : Fin (n - 1)) : Submodule.span ℝ ((fun (j : Fin (n - 1)) => iteratedDeriv (↑j + 1) (c ∘ φ) t) '' Set.Iic i) = Submodule.span ℝ ((fun (j : Fin (n - 1)) => iteratedDeriv (↑j + 1) c (φ t)) '' Set.Iic i)

theorem SpaceCurves.frenetFrame_inner_pos_reparametrized {n : ℕ} (c : ℝ → EuclideanSpace ℝ (Fin n)) (φ : ℝ → ℝ) (hc : IsFrenetCurve c) (hφ : ContDiff ℝ ⊤ φ) (hφ' : ∀ (t : ℝ), 0 < deriv φ t) (t : ℝ) (i : Fin (n - 1)) : 0 < inner ℝ (frenetFrame c hc (φ t) ⟨↑i, ⋯⟩) (iteratedDeriv (↑i + 1) (c ∘ φ) t)

theorem SpaceCurves.orthonormalBasis_eq_of_agree_on_prefix {n : ℕ} (b₁ b₂ : OrthonormalBasis (Fin n) ℝ (EuclideanSpace ℝ (Fin n))) (h : ∀ (i : Fin n), ↑i < n - 1 → b₁ i = b₂ i) (i : Fin n) : b₁ i = b₂ i

theorem SpaceCurves.frenet_frame_reparametrization_invariant {n : ℕ} (c : ℝ → EuclideanSpace ℝ (Fin n)) (φ : ℝ → ℝ) (hc : IsFrenetCurve c) (hφ : ContDiff ℝ ⊤ φ) (hφ' : ∀ (t : ℝ), 0 < deriv φ t) (t : ℝ) : frenetFrame (c ∘ φ) ⋯ t = frenetFrame c hc (φ t)