Documentation

Lean 4 Proof

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

Dependency Graph

Location

thesis/CESProofs/Foundations/InformationGeometry.lean:530

Module Section

Information Geometry of CES:

In the same file