Documentation

Lean 4 Proof

theorem slerp_at_one {s0j s1j θ : ℝ} (hs : 0 ≤ s1j) (hθ : Real.sin θ ≠ 0) :
    slerpShareComponent s0j s1j θ 1 = s1j := by
  simp only [slerpShareComponent]
  simp only [sub_self, zero_mul, Real.sin_zero, zero_div, zero_mul, zero_add, one_mul]
  rw [div_self hθ, one_mul, Real.sq_sqrt hs]

Dependency Graph

Location

thesis/CESProofs/Foundations/InformationGeometry.lean:537

Module Section

Information Geometry of CES:

In the same file