theorem SturmHurwitz.sin_half_diff_ne_zero {t₁ t₂ : ℝ} (ht₁ : t₁ ∈ Set.Ico 0 (2 * Real.pi)) (ht₂ : t₂ ∈ Set.Ico 0 (2 * Real.pi)) (hne : t₁ ≠ t₂) : Real.sin ((t₁ - t₂) / 2) ≠ 0

theorem SturmHurwitz.sturm_hurwitz (f : ℝ → ℝ) (hcont : Continuous f) (hper : ∀ (t : ℝ), f (t + 2 * Real.pi) = f t) (h0 : ∫ (t : ℝ) in 0..2 * Real.pi, f t = 0) (hcos : ∫ (t : ℝ) in 0..2 * Real.pi, f t * Real.cos t = 0) (hsin : ∫ (t : ℝ) in 0..2 * Real.pi, f t * Real.sin t = 0) : ∃ (t₁ : ℝ) (t₂ : ℝ) (t₃ : ℝ) (t₄ : ℝ), 0 ≤ t₁ ∧ t₁ < t₂ ∧ t₂ < t₃ ∧ t₃ < t₄ ∧ t₄ < 2 * Real.pi ∧ f t₁ = 0 ∧ f t₂ = 0 ∧ f t₃ = 0 ∧ f t₄ = 0

theorem SturmHurwitz.periodic_deriv (g : ℝ → ℝ) (hdiff : Differentiable ℝ g) (hper : ∀ (t : ℝ), g (t + 2 * Real.pi) = g t) (t : ℝ) : deriv g (t + 2 * Real.pi) = deriv g t

theorem SturmHurwitz.ibp_deriv_cos (g : ℝ → ℝ) (hdiff : Differentiable ℝ g) (hcont_g' : Continuous (deriv g)) (hcont_g : Continuous g) (hper : ∀ (t : ℝ), g (t + 2 * Real.pi) = g t) : ∫ (t : ℝ) in 0..2 * Real.pi, deriv g t * Real.cos t = ∫ (t : ℝ) in 0..2 * Real.pi, g t * Real.sin t

theorem SturmHurwitz.ibp_deriv_sin (g : ℝ → ℝ) (hdiff : Differentiable ℝ g) (hcont_g' : Continuous (deriv g)) (hcont_g : Continuous g) : ∫ (t : ℝ) in 0..2 * Real.pi, deriv g t * Real.sin t = -∫ (t : ℝ) in 0..2 * Real.pi, g t * Real.cos t

theorem SturmHurwitz.h_plus_h''_four_critical_points (h : ℝ → ℝ) (hsmooth : ContDiff ℝ ⊤ h) (hper : ∀ (t : ℝ), h (t + 2 * Real.pi) = h t) : ∃ (t₁ : ℝ) (t₂ : ℝ) (t₃ : ℝ) (t₄ : ℝ), 0 ≤ t₁ ∧ t₁ < t₂ ∧ t₂ < t₃ ∧ t₃ < t₄ ∧ t₄ < 2 * Real.pi ∧ deriv (fun (t : ℝ) => h t + deriv (deriv h) t) t₁ = 0 ∧ deriv (fun (t : ℝ) => h t + deriv (deriv h) t) t₂ = 0 ∧ deriv (fun (t : ℝ) => h t + deriv (deriv h) t) t₃ = 0 ∧ deriv (fun (t : ℝ) => h t + deriv (deriv h) t) t₄ = 0

theorem FourVertex.angle_parametrization (c : ℝ → Fin 2 → ℝ) (T : ℝ) (hc : ClosedCurves.IsSimpleClosedCurve c T) (hpos : ∀ (t : ℝ), ClosedCurves.curvature c t > 0) : ∃ (d : ℝ → Fin 2 → ℝ), ClosedCurves.IsClosedCurve d (2 * Real.pi) ∧ (∀ (t : ℝ), ClosedCurves.curvature d t > 0) ∧ (∀ (t : ℝ), ‖deriv d t‖⁻¹ • deriv d t = ![Real.cos t, Real.sin t]) ∧ ∀ (t : ℝ), ClosedCurves.curvature d t = ‖deriv d t‖⁻¹

theorem FourVertex.four_vertex_from_lemmas (c : ℝ → Fin 2 → ℝ) (T : ℝ) (d : ℝ → Fin 2 → ℝ) (hc : ClosedCurves.IsSimpleClosedCurve c T) (hpos : ∀ (t : ℝ), ClosedCurves.curvature c t > 0) (hsmooth_κ : ContDiff ℝ ⊤ (ClosedCurves.curvature c)) (hd_closed : ClosedCurves.IsClosedCurve d (2 * Real.pi)) (hd_pos : ∀ (t : ℝ), ClosedCurves.curvature d t > 0) (hd_unit : ∀ (t : ℝ), ‖deriv d t‖⁻¹ • deriv d t = ![Real.cos t, Real.sin t]) (hd_κ : ∀ (t : ℝ), ClosedCurves.curvature d t = ‖deriv d t‖⁻¹) : ∃ (t₁ : ℝ) (t₂ : ℝ) (t₃ : ℝ) (t₄ : ℝ), 0 ≤ t₁ ∧ t₁ < t₂ ∧ t₂ < t₃ ∧ t₃ < t₄ ∧ t₄ < T ∧ deriv (ClosedCurves.curvature c) t₁ = 0 ∧ deriv (ClosedCurves.curvature c) t₂ = 0 ∧ deriv (ClosedCurves.curvature c) t₃ = 0 ∧ deriv (ClosedCurves.curvature c) t₄ = 0

theorem FourVertex.four_vertex_theorem (c : ℝ → Fin 2 → ℝ) (T : ℝ) (hc : ClosedCurves.IsSimpleClosedCurve c T) (hpos : ∀ (t : ℝ), ClosedCurves.curvature c t > 0) (hsmooth_κ : ContDiff ℝ ⊤ (ClosedCurves.curvature c)) : ∃ (t₁ : ℝ) (t₂ : ℝ) (t₃ : ℝ) (t₄ : ℝ), 0 ≤ t₁ ∧ t₁ < t₂ ∧ t₂ < t₃ ∧ t₃ < t₄ ∧ t₄ < T ∧ deriv (ClosedCurves.curvature c) t₁ = 0 ∧ deriv (ClosedCurves.curvature c) t₂ = 0 ∧ deriv (ClosedCurves.curvature c) t₃ = 0 ∧ deriv (ClosedCurves.curvature c) t₄ = 0