Documentation

Lean 4 Proof

def slerpShareComponent (s0j s1j : ℝ) (θ t : ℝ) : ℝ :=
  (Real.sin ((1 - t) * θ) / Real.sin θ * Real.sqrt s0j +
   Real.sin (t * θ) / Real.sin θ * Real.sqrt s1j) ^ 2

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/InformationGeometry.lean:518

Module Section

Information Geometry of CES:

In the same file