structure ClosedCurves.IsClosedCurve (c : ℝ → Fin 2 → ℝ) (T : ℝ) : Prop

• smooth : ContDiff ℝ ⊤ c
• period_pos : T > 0
• periodic (t : ℝ) : c (t + T) = c t
• regular (t : ℝ) : deriv c t ≠ 0

def ClosedCurves.IsSimpleClosedCurve (c : ℝ → Fin 2 → ℝ) (T : ℝ) : Prop

def ClosedCurves.IsConvexCurve (c : ℝ → Fin 2 → ℝ) (T : ℝ) : Prop

noncomputable def ClosedCurves.toEuclidean (c : ℝ → Fin 2 → ℝ) : ℝ → EuclideanSpace ℝ (Fin 2)

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

noncomputable def ClosedCurves.totalCurvature (c : ℝ → Fin 2 → ℝ) (T : ℝ) : ℝ

theorem ClosedCurves.jordan_curve_theorem (c : ℝ → Fin 2 → ℝ) (T : ℝ) : IsSimpleClosedCurve c T → ∃ (U : Set (Fin 2 → ℝ)) (V : Set (Fin 2 → ℝ)), IsOpen U ∧ IsOpen V ∧ IsConnected U ∧ IsConnected V ∧ Disjoint U V ∧ U ∪ V = (Set.range c)ᶜ ∧ Bornology.IsBounded U ∧ ¬Bornology.IsBounded V

theorem ClosedCurves.toEuclidean_deriv_norm (c : ℝ → Fin 2 → ℝ) (hc : ContDiff ℝ ⊤ c) (t : ℝ) : ‖deriv (toEuclidean c) t‖ = ‖deriv c t‖

theorem ClosedCurves.curvature_comp_reparam (c : ℝ → Fin 2 → ℝ) (φ : ℝ → ℝ) (hc : ContDiff ℝ ⊤ c) (hφ : ContDiff ℝ ⊤ φ) (hφ_pos : ∀ (t : ℝ), 0 < deriv φ t) (hreg : ∀ (t : ℝ), deriv c (φ t) ≠ 0) (t : ℝ) : curvature (c ∘ φ) t = curvature c (φ t)

theorem ClosedCurves.totalCurvature_integrand_periodic (c : ℝ → Fin 2 → ℝ) (T : ℝ) (hc : ContDiff ℝ ⊤ c) (hperiodic : ∀ (t : ℝ), c (t + T) = c t) : Function.Periodic (fun (t : ℝ) => curvature c t * ‖deriv (toEuclidean c) t‖) T

theorem ClosedCurves.curvature_comp_continuous (c : ℝ → Fin 2 → ℝ) (φ : ℝ → ℝ) (hc : ContDiff ℝ ⊤ c) (hφ : ContDiff ℝ ⊤ φ) (hreg : ∀ (s : ℝ), deriv c (φ s) ≠ 0) : Continuous fun (s : ℝ) => curvature c (φ s)

theorem ClosedCurves.totalCurvature_reparam_eq (c : ℝ → Fin 2 → ℝ) (φ ψ : ℝ → ℝ) (T : ℝ) (hc_smooth : ContDiff ℝ ⊤ c) (hφ_smooth : ContDiff ℝ ⊤ φ) (hψ_smooth : ContDiff ℝ ⊤ ψ) (hφ_left : Function.LeftInverse φ ψ) (hφ_right : Function.RightInverse φ ψ) (hψ_deriv : ∀ (t : ℝ), deriv ψ t = ‖deriv c t‖) (hψ_pos : ∀ (t : ℝ), 0 < deriv ψ t) (hψ_periodic_shift : ∀ (t : ℝ), ψ (t + T) = ψ t + ∫ (u : ℝ) in 0..T, ‖deriv c u‖) (hd_unit : ∀ (t : ℝ), ‖deriv (c ∘ φ) t‖ = 1) (hc_periodic : ∀ (t : ℝ), c (t + T) = c t) : totalCurvature (c ∘ φ) (∫ (u : ℝ) in 0..T, ‖deriv c u‖) = totalCurvature c T

theorem ClosedCurves.deriv_periodic_of_closed (c : ℝ → Fin 2 → ℝ) (T : ℝ) (hc : IsClosedCurve c T) (t : ℝ) : deriv c (t + T) = deriv c t

theorem ClosedCurves.norm_deriv_periodic_of_closed (c : ℝ → Fin 2 → ℝ) (T : ℝ) (hc : IsClosedCurve c T) (t : ℝ) : ‖deriv c (t + T)‖ = ‖deriv c t‖

theorem ClosedCurves.unit_speed_reparam_closed (c : ℝ → Fin 2 → ℝ) (T : ℝ) (hc : IsClosedCurve c T) : have L := ∫ (t : ℝ) in 0..T, ‖deriv c t‖; ∃ (d : ℝ → Fin 2 → ℝ), IsClosedCurve d L ∧ (∀ (t : ℝ), ‖deriv d t‖ = 1) ∧ totalCurvature d L = totalCurvature c T

noncomputable def ClosedCurves.unitTangent (c : ℝ → Fin 2 → ℝ) (t : ℝ) : Fin 2 → ℝ

noncomputable def ClosedCurves.rotationNumber (c : ℝ → Fin 2 → ℝ) (T : ℝ) : ℝ

theorem ClosedCurves.curvature_speed_eq_det2_unitTangent (c : ℝ → Fin 2 → ℝ) (t : ℝ) (hsmooth : ContDiff ℝ ⊤ c) (hc' : deriv c t ≠ 0) : curvature c t * ‖deriv (toEuclidean c) t‖ = DegreeTheory.det2 (unitTangent c t) (deriv (unitTangent c) t)

theorem ClosedCurves.total_curvature_eq_two_pi_degree (c : ℝ → Fin 2 → ℝ) (T : ℝ) (hc : IsClosedCurve c T) : totalCurvature c T = 2 * Real.pi * DegreeTheory.degreeReal (unitTangent c) T

theorem ClosedCurves.rotationNumber_eq_degree (c : ℝ → Fin 2 → ℝ) (T : ℝ) (hc : IsClosedCurve c T) : rotationNumber c T = DegreeTheory.degreeReal (unitTangent c) T

theorem ClosedCurves.unitTangent_smooth (c : ℝ → Fin 2 → ℝ) (hc : ContDiff ℝ ⊤ c) (hreg : ∀ (t : ℝ), deriv c t ≠ 0) : ContDiff ℝ ⊤ (unitTangent c)

theorem ClosedCurves.unitTangent_on_unit_circle (c : ℝ → Fin 2 → ℝ) (T : ℝ) (hc : IsClosedCurve c T) : DegreeTheory.OnUnitCircle (unitTangent c)

theorem ClosedCurves.unitTangent_periodic (c : ℝ → Fin 2 → ℝ) (T : ℝ) (hc : IsClosedCurve c T) (t : ℝ) : unitTangent c (t + T) = unitTangent c t

theorem ClosedCurves.rotationNumber_is_integer (c : ℝ → Fin 2 → ℝ) (T : ℝ) (hc : IsClosedCurve c T) : ∃ (k : ℤ), rotationNumber c T = ↑k

theorem ClosedCurves.det2_unitTangent_deriv_eq_curvature_speed (c : ℝ → Fin 2 → ℝ) (t : ℝ) (p : Fin 2 → ℝ) (hsmooth : ContDiff ℝ ⊤ c) (hc' : deriv c t ≠ 0) (hfp : unitTangent c t = p) : DegreeTheory.det2 p (deriv (unitTangent c) t) = curvature c t * ‖deriv (toEuclidean c) t‖

theorem ClosedCurves.norm_deriv_toEuclidean_pos (c : ℝ → Fin 2 → ℝ) (t : ℝ) (hsmooth : ContDiff ℝ ⊤ c) (hc' : deriv c t ≠ 0) : ‖deriv (toEuclidean c) t‖ > 0

theorem ClosedCurves.sign_det2_unitTangent_eq_sign_curvature (c : ℝ → Fin 2 → ℝ) (t : ℝ) (p : Fin 2 → ℝ) (hsmooth : ContDiff ℝ ⊤ c) (hc' : deriv c t ≠ 0) (hfp : unitTangent c t = p) : (DegreeTheory.det2 p (deriv (unitTangent c) t)).sign = (curvature c t).sign

theorem ClosedCurves.unitTangent_eq_e1_iff (c : ℝ → Fin 2 → ℝ) (t : ℝ) (hsmooth : ContDiff ℝ ⊤ c) (hc' : deriv c t ≠ 0) : (unitTangent c t = fun (i : Fin 2) => if i = 0 then 1 else 0) ↔ deriv c t 1 = 0 ∧ deriv c t 0 > 0

theorem ClosedCurves.rotation_number_eq_signed_curvature_sum (c : ℝ → Fin 2 → ℝ) (T : ℝ) (hc : IsClosedCurve c T) (specialPts : Finset ℝ) (hpts_range : ∀ t ∈ specialPts, 0 ≤ t ∧ t < T) (hpts_cond : ∀ t ∈ specialPts, deriv c t 1 = 0 ∧ deriv c t 0 > 0) (hpts_complete : ∀ (t : ℝ), 0 ≤ t → t < T → deriv c t 1 = 0 → deriv c t 0 > 0 → t ∈ specialPts) (hcurv_ne : ∀ t ∈ specialPts, curvature c t ≠ 0) : rotationNumber c T = ∑ t ∈ specialPts, (curvature c t).sign

theorem ClosedCurves.convex_iff_curvature_no_sign_change (c : ℝ → Fin 2 → ℝ) (T : ℝ) (hc : IsSimpleClosedCurve c T) : IsConvexCurve c T ↔ (∀ (t : ℝ), curvature c t ≥ 0) ∨ ∀ (t : ℝ), curvature c t ≤ 0

noncomputable def ClosedCurves.det2 (a b : Fin 2 → ℝ) : ℝ

theorem ClosedCurves.whitney_formula (c : ℝ → Fin 2 → ℝ) (T : ℝ) (hc : IsClosedCurve c T) (hmin : ∀ (t : ℝ), c 0 1 ≤ c t 1) (crossings : Finset (ℝ × ℝ)) (hcross : ∀ p ∈ crossings, 0 ≤ p.1 ∧ p.1 < p.2 ∧ p.2 < T ∧ c p.1 = c p.2) (hcross_complete : ∀ (s t : ℝ), 0 ≤ s → s < t → t < T → c s = c t → (s, t) ∈ crossings) (hnormal : ∀ p ∈ crossings, det2 (deriv c p.1) (deriv c p.2) ≠ 0) : totalCurvature c T / (2 * Real.pi) = (deriv c 0 0).sign - ∑ p ∈ crossings, (det2 (deriv c p.1) (deriv c p.2)).sign

theorem ClosedCurves.totalCurvature_shift (c : ℝ → Fin 2 → ℝ) (T t₀ : ℝ) (hc : IsClosedCurve c T) : totalCurvature (fun (t : ℝ) => c (t + t₀)) T = totalCurvature c T

theorem ClosedCurves.periodic_global_min_of_minOn {f : ℝ → ℝ} {T t₀ : ℝ} (hT : 0 < T) (hper : Function.Periodic f T) (hmin : IsMinOn f (Set.Icc 0 T) t₀) (s : ℝ) : f t₀ ≤ f s

theorem ClosedCurves.hopf_umlaufsatz (c : ℝ → Fin 2 → ℝ) (T : ℝ) (hc : IsSimpleClosedCurve c T) : rotationNumber c T = 1 ∨ rotationNumber c T = -1

theorem ClosedCurves.totalCurvature_simple_closed_eq_pm_two_pi (c : ℝ → Fin 2 → ℝ) (T : ℝ) (hc : IsSimpleClosedCurve c T) : totalCurvature c T = 2 * Real.pi ∨ totalCurvature c T = -(2 * Real.pi)

theorem ClosedCurves.rotationNumber_ne_zero_general (c : ℝ → Fin 2 → ℝ) (T : ℝ) (hc : IsClosedCurve c T) : rotationNumber c T ≠ 0

theorem ClosedCurves.total_absolute_curvature_ge_two_pi (c : ℝ → Fin 2 → ℝ) (T : ℝ) (hc : IsClosedCurve c T) : ∫ (t : ℝ) in 0..T, |curvature c t| * ‖deriv (toEuclidean c) t‖ ≥ 2 * Real.pi

theorem ClosedCurves.curvature_integrand_continuous (c : ℝ → Fin 2 → ℝ) (hc : ContDiff ℝ ⊤ c) (hreg : ∀ (t : ℝ), deriv c t ≠ 0) : Continuous fun (t : ℝ) => curvature c t * ‖deriv (toEuclidean c) t‖

theorem ClosedCurves.toEuclidean_deriv_eq_zero (c : ℝ → Fin 2 → ℝ) (hc : ContDiff ℝ ⊤ c) (t : ℝ) : deriv (toEuclidean c) t = 0 ↔ deriv c t = 0

theorem ClosedCurves.unitTangent_onUnitCircle (c : ℝ → Fin 2 → ℝ) (hc : ContDiff ℝ ⊤ c) (hreg : ∀ (t : ℝ), deriv c t ≠ 0) : DegreeTheory.OnUnitCircle (unitTangent c)

theorem ClosedCurves.angle_function_hasDerivAt_angularVelocity (c : ℝ → Fin 2 → ℝ) (θ : ℝ → ℝ) (hc : ContDiff ℝ ⊤ c) (hreg : ∀ (t : ℝ), deriv c t ≠ 0) (hθ : DegreeTheory.IsAngleFunction (unitTangent c) θ) (t : ℝ) : HasDerivAt θ (DegreeTheory.angularVelocity (unitTangent c) t) t

theorem ClosedCurves.angularVelocity_unitTangent_pos (c : ℝ → Fin 2 → ℝ) (t : ℝ) (hc : ContDiff ℝ ⊤ c) (hreg : ∀ (t : ℝ), deriv c t ≠ 0) (hκ_pos : curvature c t > 0) : DegreeTheory.angularVelocity (unitTangent c) t > 0

theorem ClosedCurves.angle_function_period_shift (c : ℝ → Fin 2 → ℝ) (T : ℝ) (θ : ℝ → ℝ) (hc : IsClosedCurve c T) (hpos : ∀ (t : ℝ), curvature c t > 0) (hθ : DegreeTheory.IsAngleFunction (unitTangent c) θ) (htc : totalCurvature c T = 2 * Real.pi) (t : ℝ) : θ (t + T) = θ t + 2 * Real.pi

theorem ClosedCurves.angle_reparam_inverse_period (φ θ : ℝ → ℝ) (T : ℝ) (hleft : Function.LeftInverse φ θ) (hright : Function.RightInverse φ θ) (hθ_shift : ∀ (t : ℝ), θ (t + T) = θ t + 2 * Real.pi) {t : ℝ} : φ (t + 2 * Real.pi) = φ t + T

theorem ClosedCurves.angle_reparam_inverse_deriv_pos (θ φ : ℝ → ℝ) (hθ_pos : ∀ (t : ℝ), 0 < deriv θ t) (hleft : Function.LeftInverse φ θ) (hright : Function.RightInverse φ θ) (hderiv : ∀ (t : ℝ), deriv φ (θ t) = (deriv θ t)⁻¹) (t : ℝ) : deriv φ t > 0

theorem ClosedCurves.comp_deriv_ne_zero (c : ℝ → Fin 2 → ℝ) (φ : ℝ → ℝ) (hc : ContDiff ℝ ⊤ c) (hφ : ContDiff ℝ ⊤ φ) {t : ℝ} (hreg : deriv c (φ t) ≠ 0) (hφ_ne : deriv φ t ≠ 0) : deriv (c ∘ φ) t ≠ 0

theorem ClosedCurves.unit_tangent_angle_reparam (c : ℝ → Fin 2 → ℝ) (φ θ : ℝ → ℝ) (t : ℝ) (hc : ContDiff ℝ ⊤ c) (hφ : ContDiff ℝ ⊤ φ) (hreg : ∀ (s : ℝ), deriv c s ≠ 0) (hφ_pos : ∀ (s : ℝ), deriv φ s > 0) (hθ : DegreeTheory.IsAngleFunction (unitTangent c) θ) (hleft : Function.LeftInverse φ θ) : ‖deriv (c ∘ φ) t‖⁻¹ • deriv (c ∘ φ) t = ![Real.cos t, Real.sin t]

theorem ClosedCurves.curvature_eq_inv_speed_of_angle_param (d : ℝ → Fin 2 → ℝ) (t : ℝ) (hd : ContDiff ℝ ⊤ d) (hreg : deriv d t ≠ 0) (hunit : ‖deriv d t‖⁻¹ • deriv d t = ![Real.cos t, Real.sin t]) : curvature d t = ‖deriv d t‖⁻¹