Documentation

Lean 4 Proof

theorem slerp_midpoint_coeff {θ : ℝ} (hθ : Real.cos (θ / 2) ≠ 0)
    (hsinθ : Real.sin θ ≠ 0) :
    Real.sin (θ / 2) / Real.sin θ = 1 / (2 * Real.cos (θ / 2)) := by
  have hdouble : Real.sin θ = 2 * Real.sin (θ / 2) * Real.cos (θ / 2) := by
    rw [← Real.sin_two_mul, two_mul (θ / 2), add_halves]
  rw [hdouble]
  have hsin : Real.sin (θ / 2) ≠ 0 := by
    intro h; rw [hdouble, h, mul_zero, zero_mul] at hsinθ; exact hsinθ rfl
  field_simp

Dependency Graph

Location

thesis/CESProofs/Foundations/InformationGeometry.lean:573

Module Section

Information Geometry of CES:

In the same file