pathFromRotation

formal source

  25
  26
  27/-- Construct recognition path from geodesic rotation using recognition profile -/
  28noncomputable def pathFromRotation (rot : TwoBranchRotation) : RecognitionPath where
  29  T := π/2 - rot.θ_s
  30  T_pos := by
  31    have ⟨_, h2⟩ := rot.θ_s_bounds
  32    linarith
  33  rate := fun ϑ => recognitionProfile (ϑ + rot.θ_s)
  34  rate_pos := by
  35    intro t ht
  36    apply recognitionProfile_pos
  37    have ⟨h1, h2⟩ := rot.θ_s_bounds
  38    constructor
  39    · -- 0 ≤ t + θ_s
  40      have := ht.1
  41      linarith
  42    · -- t + θ_s ≤ π/2
  43      have ht' : t ≤ π/2 - rot.θ_s := ht.2
  44      have := add_le_add_right ht' rot.θ_s
  45      simpa [add_comm, add_left_comm, add_assoc, sub_eq_add_neg] using this
  46
  47/-- The integral of tan from θ_s to π/2 equals -ln(sin θ_s) -/
  48theorem integral_cot_from_theta (θ_s : ℝ) (hθ : 0 < θ_s ∧ θ_s < π/2) :
  49  ∫ θ in θ_s..(π/2), Real.cot θ = - Real.log (Real.sin θ_s) := by
  50  -- Standard calculus result: ∫ cot θ dθ = log(sin θ) + C.
  51  -- We prove it via FTC on `f(θ) = log(sin θ)` over `[θ_s, π/2]`.
  52  let f : ℝ → ℝ := fun θ => Real.log (Real.sin θ)
  53
  54  have hpi2ltpi : (Real.pi / 2 : ℝ) < Real.pi := by nlinarith [Real.pi_pos]
  55
  56  have hsin_ne0_uIcc : ∀ x ∈ Set.uIcc θ_s (π/2), Real.sin x ≠ 0 := by
  57    intro x hx
  58    have hx' : θ_s ≤ x ∧ x ≤ π/2 := by