pith. machine review for the scientific record. sign in
def definition def or abbrev

pathFromRotation

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  28noncomputable def pathFromRotation (rot : TwoBranchRotation) : RecognitionPath where
  29  T := π/2 - rot.θ_s

proof body

Definition body.

  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) -/

used by (5)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (15)

Lean names referenced from this declaration's body.