def PlaneCurves.det2 (v w : EuclideanSpace ℝ (Fin 2)) : ℝ

theorem PlaneCurves.det2_antisymm (v w : EuclideanSpace ℝ (Fin 2)) : det2 v w = -det2 w v

theorem PlaneCurves.det2_self (v : EuclideanSpace ℝ (Fin 2)) : det2 v v = 0

structure PlaneCurves.IsRegularCurve (c : ℝ → EuclideanSpace ℝ (Fin 2)) (S : Set ℝ) : Prop

• smooth : ContDiff ℝ ⊤ c
• deriv_ne_zero (t : ℝ) : t ∈ S → deriv c t ≠ 0

noncomputable def PlaneCurves.curvature (c : ℝ → EuclideanSpace ℝ (Fin 2)) (t : ℝ) : ℝ

noncomputable def PlaneCurves.J (v : EuclideanSpace ℝ (Fin 2)) : EuclideanSpace ℝ (Fin 2)

@[simp]

theorem PlaneCurves.J_apply_zero (v : EuclideanSpace ℝ (Fin 2)) : (J v).ofLp 0 = -v.ofLp 1

@[simp]

theorem PlaneCurves.J_apply_one (v : EuclideanSpace ℝ (Fin 2)) : (J v).ofLp 1 = v.ofLp 0

theorem PlaneCurves.inner_eq_coord (v w : EuclideanSpace ℝ (Fin 2)) : inner ℝ v w = v.ofLp 0 * w.ofLp 0 + v.ofLp 1 * w.ofLp 1

theorem PlaneCurves.deriv_eq_det2_smul_J_of_norm_eq_one (f : ℝ → EuclideanSpace ℝ (Fin 2)) (hf : ContDiff ℝ ⊤ f) (hunit : ∀ (t : ℝ), ‖f t‖ = 1) (t : ℝ) : deriv f t = det2 (f t) (deriv f t) • J (f t)

theorem PlaneCurves.J_smul (a : ℝ) (v : EuclideanSpace ℝ (Fin 2)) : J (a • v) = a • J v

theorem PlaneCurves.det2_smul_left (a : ℝ) (v w : EuclideanSpace ℝ (Fin 2)) : det2 (a • v) w = a * det2 v w

theorem PlaneCurves.det2_add_right (v w₁ w₂ : EuclideanSpace ℝ (Fin 2)) : det2 v (w₁ + w₂) = det2 v w₁ + det2 v w₂

theorem PlaneCurves.det2_smul_right (a : ℝ) (v w : EuclideanSpace ℝ (Fin 2)) : det2 v (a • w) = a * det2 v w

theorem PlaneCurves.det2_unit_tangent_deriv (v w : EuclideanSpace ℝ (Fin 2)) (α : ℝ) (hv : ‖v‖ ≠ 0) : det2 (‖v‖⁻¹ • v) (‖v‖⁻¹ • w + α • v) * ‖v‖⁻¹ = det2 v w / ‖v‖ ^ 3

theorem PlaneCurves.frenet_equation (c : ℝ → EuclideanSpace ℝ (Fin 2)) (hc : ContDiff ℝ ⊤ c) (hreg : ∀ (t : ℝ), deriv c t ≠ 0) (t : ℝ) : deriv (fun (s : ℝ) => ‖deriv c s‖⁻¹ • deriv c s) t = curvature c t • J (deriv c t)

theorem PlaneCurves.J_J (v : EuclideanSpace ℝ (Fin 2)) : J (J v) = -v

theorem PlaneCurves.norm_J (v : EuclideanSpace ℝ (Fin 2)) : ‖J v‖ = ‖v‖

theorem PlaneCurves.J_add (v w : EuclideanSpace ℝ (Fin 2)) : J (v + w) = J v + J w

noncomputable def PlaneCurves.JLinearMap : EuclideanSpace ℝ (Fin 2) →ₗ[ℝ] EuclideanSpace ℝ (Fin 2)

noncomputable def PlaneCurves.JContinuous : EuclideanSpace ℝ (Fin 2) →L[ℝ] EuclideanSpace ℝ (Fin 2)

theorem PlaneCurves.J_hasDerivAt (f : ℝ → EuclideanSpace ℝ (Fin 2)) (f' : EuclideanSpace ℝ (Fin 2)) (t : ℝ) (hf : HasDerivAt f f' t) : HasDerivAt (fun (s : ℝ) => J (f s)) (J f') t

theorem PlaneCurves.constant_curvature_is_circle (c : ℝ → EuclideanSpace ℝ (Fin 2)) (hc : ContDiff ℝ ⊤ c) (hreg : ∀ (t : ℝ), deriv c t ≠ 0) (R : ℝ) (hR : R ≠ 0) (hκ : ∀ (t : ℝ), curvature c t = R⁻¹) : ∃ (center : EuclideanSpace ℝ (Fin 2)), ∀ (t : ℝ), ‖c t - center‖ = |R|

@[reducible, inline]

abbrev PlaneCurves.R2 : Type

noncomputable def PlaneCurves.hessianVec (F : R2 → ℝ) (x v : R2) : R2

theorem PlaneCurves.det2_J_eq_neg_inner (v w : EuclideanSpace ℝ (Fin 2)) : det2 (J v) w = -inner ℝ v w

theorem PlaneCurves.inner_J_eq_det2 (v w : EuclideanSpace ℝ (Fin 2)) : inner ℝ (J v) w = det2 v w

theorem PlaneCurves.orthog_proportional_J (v w : EuclideanSpace ℝ (Fin 2)) (hv : v ≠ 0) (horthog : inner ℝ v w = 0) : w = (det2 v w / ‖v‖ ^ 2) • J v

theorem PlaneCurves.level_set_orthogonality (F : R2 → ℝ) (c : ℝ → R2) (a : ℝ) (hF : ContDiff ℝ ⊤ F) (hc : ContDiff ℝ ⊤ c) (hlevel : ∀ (t : ℝ), F (c t) = a) (t : ℝ) : (fderiv ℝ F (c t)) (deriv c t) = 0

theorem PlaneCurves.level_set_gradient_orthogonality (F : R2 → ℝ) (c : ℝ → R2) (a : ℝ) (hF : ContDiff ℝ ⊤ F) (hc : ContDiff ℝ ⊤ c) (hlevel : ∀ (t : ℝ), F (c t) = a) (t : ℝ) : inner ℝ (gradient F (c t)) (deriv c t) = 0

theorem PlaneCurves.second_diff_level_set (F : R2 → ℝ) (c : ℝ → R2) (a : ℝ) (hF : ContDiff ℝ ⊤ F) (hc : ContDiff ℝ ⊤ c) (hlevel : ∀ (t : ℝ), F (c t) = a) (t : ℝ) : inner ℝ (hessianVec F (c t) (deriv c t)) (deriv c t) + inner ℝ (gradient F (c t)) (deriv (deriv c) t) = 0

theorem PlaneCurves.curvature_level_set (F : R2 → ℝ) (c : ℝ → R2) (a t : ℝ) (hF : ContDiff ℝ ⊤ F) (hc : ContDiff ℝ ⊤ c) (hreg : ∀ (t : ℝ), deriv c t ≠ 0) (hlevel : ∀ (t : ℝ), F (c t) = a) (hgrad : gradient F (c t) ≠ 0) (hpos : det2 (gradient F (c t)) (deriv c t) > 0) : curvature c t = inner ℝ (J (gradient F (c t))) (hessianVec F (c t) (J (gradient F (c t)))) / ‖gradient F (c t)‖ ^ 3

theorem PlaneCurves.curvature_level_set_neg (F : R2 → ℝ) (c : ℝ → R2) (a t : ℝ) (hF : ContDiff ℝ ⊤ F) (hc : ContDiff ℝ ⊤ c) (hreg : ∀ (t : ℝ), deriv c t ≠ 0) (hlevel : ∀ (t : ℝ), F (c t) = a) (hgrad : gradient F (c t) ≠ 0) (h_neg : det2 (gradient F (c t)) (deriv c t) < 0) : -curvature c t = inner ℝ (J (gradient F (c t))) (hessianVec F (c t) (J (gradient F (c t)))) / ‖gradient F (c t)‖ ^ 3

theorem PlaneCurves.curvature_level_set_full (F : R2 → ℝ) (c : ℝ → R2) (a t : ℝ) (hF : ContDiff ℝ ⊤ F) (hc : ContDiff ℝ ⊤ c) (hreg : ∀ (t : ℝ), deriv c t ≠ 0) (hlevel : ∀ (t : ℝ), F (c t) = a) (hgrad : gradient F (c t) ≠ 0) (hdet_ne : det2 (gradient F (c t)) (deriv c t) ≠ 0) : curvature c t * ‖gradient F (c t)‖ ^ 3 * |det2 (gradient F (c t)) (deriv c t)| = det2 (gradient F (c t)) (deriv c t) * inner ℝ (J (gradient F (c t))) (hessianVec F (c t) (J (gradient F (c t))))

theorem PlaneCurves.curvature_reparametrization (c : ℝ → EuclideanSpace ℝ (Fin 2)) (ψ : ℝ → ℝ) (hc : ContDiff ℝ ⊤ c) (hψ : ContDiff ℝ ⊤ ψ) (hreg : ∀ (t : ℝ), deriv c (ψ t) ≠ 0) (hψ' : ∀ (t : ℝ), deriv ψ t > 0) (t : ℝ) : curvature (c ∘ ψ) t = curvature c (ψ t)

theorem PlaneCurves.exists_smul_of_det2_eq_zero (u v : EuclideanSpace ℝ (Fin 2)) (hv : v ≠ 0) (hdet : det2 u v = 0) : ∃ (s : ℝ), u = s • v

theorem PlaneCurves.det2_sub_left (v₁ v₂ w : EuclideanSpace ℝ (Fin 2)) : det2 (v₁ - v₂) w = det2 v₁ w - det2 v₂ w

theorem PlaneCurves.zero_curvature_is_line (c : ℝ → EuclideanSpace ℝ (Fin 2)) (hc : ContDiff ℝ ⊤ c) (hreg : ∀ (t : ℝ), deriv c t ≠ 0) (hzero : ∀ (t : ℝ), curvature c t = 0) : ∃ (p : EuclideanSpace ℝ (Fin 2)) (v : EuclideanSpace ℝ (Fin 2)), ∀ (t : ℝ), ∃ (s : ℝ), c t = p + s • v

theorem PlaneCurves.deriv_toLp_comp {f : ℝ → Fin 2 → ℝ} {t : ℝ} (hf : DifferentiableAt ℝ f t) : deriv (fun (s : ℝ) => WithLp.toLp 2 (f s)) t = WithLp.toLp 2 (deriv f t)

theorem PlaneCurves.deriv_graph_curve (f : ℝ → ℝ) (hf : ContDiff ℝ ⊤ f) (t : ℝ) : deriv (fun (s : ℝ) => !₂[s, f s]) t = !₂[1, deriv f t]

theorem PlaneCurves.deriv2_graph_curve (f : ℝ → ℝ) (hf : ContDiff ℝ ⊤ f) (t : ℝ) : deriv (deriv fun (s : ℝ) => !₂[s, f s]) t = !₂[0, deriv (deriv f) t]

theorem PlaneCurves.curvature_graph (f : ℝ → ℝ) (hf : ContDiff ℝ ⊤ f) (t : ℝ) : curvature (fun (t : ℝ) => !₂[t, f t]) t = deriv (deriv f) t / (1 + deriv f t ^ 2) ^ (3 / 2)

theorem PlaneCurves.curvature_unit_speed (c : ℝ → EuclideanSpace ℝ (Fin 2)) (_hc : ContDiff ℝ ⊤ c) (hunit : ∀ (t : ℝ), ‖deriv c t‖ = 1) (t : ℝ) : curvature c t = det2 (deriv c t) (deriv (deriv c) t)

theorem PlaneCurves.unit_speed_second_deriv (c : ℝ → EuclideanSpace ℝ (Fin 2)) (hc : ContDiff ℝ ⊤ c) (hunit : ∀ (t : ℝ), ‖deriv c t‖ = 1) (t : ℝ) : deriv (deriv c) t = curvature c t • J (deriv c t)

theorem PlaneCurves.curvature_abs_eq_norm_second_deriv (c : ℝ → EuclideanSpace ℝ (Fin 2)) (hc : ContDiff ℝ ⊤ c) (hunit : ∀ (t : ℝ), ‖deriv c t‖ = 1) (t : ℝ) : |curvature c t| = ‖deriv (deriv c) t‖

theorem PlaneCurves.curvature_unit_speed_characterization (c : ℝ → EuclideanSpace ℝ (Fin 2)) (hc : ContDiff ℝ ⊤ c) (hunit : ∀ (t : ℝ), ‖deriv c t‖ = 1) (t : ℝ) : curvature c t = det2 (deriv c t) (deriv (deriv c) t) ∧ deriv (deriv c) t = curvature c t • J (deriv c t) ∧ |curvature c t| = ‖deriv (deriv c) t‖

theorem PlaneCurves.analyticAt_antideriv {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {f : ℝ → F} {x : ℝ} (hf : AnalyticAt ℝ f x) (a : ℝ) : AnalyticAt ℝ (fun (t : ℝ) => ∫ (s : ℝ) in a..t, f s) x

theorem PlaneCurves.contDiff_top_antideriv {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {f : ℝ → F} (hf : ContDiff ℝ ⊤ f) (a : ℝ) : ContDiff ℝ ⊤ fun (t : ℝ) => ∫ (s : ℝ) in a..t, f s

theorem PlaneCurves.hasDerivAt_euclidean_pair {f g : ℝ → ℝ} {f' g' t : ℝ} (hf : HasDerivAt f f' t) (hg : HasDerivAt g g' t) : HasDerivAt (fun (s : ℝ) => (EuclideanSpace.equiv (Fin 2) ℝ).symm ![f s, g s]) ((EuclideanSpace.equiv (Fin 2) ℝ).symm ![f', g']) t

theorem PlaneCurves.fundamental_theorem_plane_curves_existence (κ : ℝ → ℝ) (hκ : ContDiff ℝ ⊤ κ) : ∃ (c : ℝ → EuclideanSpace ℝ (Fin 2)), ContDiff ℝ ⊤ c ∧ (∀ (t : ℝ), ‖deriv c t‖ = 1) ∧ ∀ (t : ℝ), curvature c t = κ t

theorem PlaneCurves.fundamental_theorem_plane_curves_uniqueness (c₁ c₂ : ℝ → EuclideanSpace ℝ (Fin 2)) (hc₁ : ContDiff ℝ ⊤ c₁) (hc₂ : ContDiff ℝ ⊤ c₂) (hunit₁ : ∀ (t : ℝ), ‖deriv c₁ t‖ = 1) (hunit₂ : ∀ (t : ℝ), ‖deriv c₂ t‖ = 1) (hκ : ∀ (t : ℝ), curvature c₁ t = curvature c₂ t) : ∃ (A : Matrix (Fin 2) (Fin 2) ℝ) (b : EuclideanSpace ℝ (Fin 2)), A.det = 1 ∧ A * A.transpose = 1 ∧ ∀ (t : ℝ), c₂ t = (EuclideanSpace.equiv (Fin 2) ℝ).symm (A.mulVec ((EuclideanSpace.equiv (Fin 2) ℝ) (c₁ t))) + b

theorem PlaneCurves.fundamental_theorem_plane_curves (κ : ℝ → ℝ) (hκ : ContDiff ℝ ⊤ κ) : (∃ (c : ℝ → EuclideanSpace ℝ (Fin 2)), ContDiff ℝ ⊤ c ∧ (∀ (t : ℝ), ‖deriv c t‖ = 1) ∧ ∀ (t : ℝ), curvature c t = κ t) ∧ ∀ (c₁ c₂ : ℝ → EuclideanSpace ℝ (Fin 2)), ContDiff ℝ ⊤ c₁ → ContDiff ℝ ⊤ c₂ → (∀ (t : ℝ), ‖deriv c₁ t‖ = 1) → (∀ (t : ℝ), ‖deriv c₂ t‖ = 1) → (∀ (t : ℝ), curvature c₁ t = κ t) → (∀ (t : ℝ), curvature c₂ t = κ t) → ∃ (A : Matrix (Fin 2) (Fin 2) ℝ) (b : EuclideanSpace ℝ (Fin 2)), A.det = 1 ∧ A * A.transpose = 1 ∧ ∀ (t : ℝ), c₂ t = (EuclideanSpace.equiv (Fin 2) ℝ).symm (A.mulVec ((EuclideanSpace.equiv (Fin 2) ℝ) (c₁ t))) + b

theorem PlaneCurves.osculating_circle (c : ℝ → EuclideanSpace ℝ (Fin 2)) (_hc : ContDiff ℝ ⊤ c) (hunit : ∀ (t : ℝ), ‖deriv c t‖ = 1) (t₀ : ℝ) (hκ : curvature c t₀ ≠ 0) : have center := c t₀ + (curvature c t₀)⁻¹ • J (deriv c t₀); have R := |(curvature c t₀)⁻¹|; R > 0 ∧ ‖c t₀ - center‖ = R ∧ inner ℝ (c t₀ - center) (deriv c t₀) = 0 ∧ R⁻¹ = |curvature c t₀| ∧ ∀ (center' : EuclideanSpace ℝ (Fin 2)), ∀ R' > 0, ‖c t₀ - center'‖ = R' → inner ℝ (c t₀ - center') (deriv c t₀) = 0 → R'⁻¹ = |curvature c t₀| → inner ℝ (center' - c t₀) (J (deriv c t₀)) * curvature c t₀ > 0 → center' = center ∧ R' = R