Documentation

Lean 4 Proof

theorem bhattacharyya_eq_cos_distance {J : ℕ} (s0 s1 : Fin J → ℝ) :
    fisherRaoDistance s0 s1 = Real.arccos (bhattacharyyaCoeff s0 s1) := rfl

Dependency Graph

Location

thesis/CESProofs/Foundations/InformationGeometry.lean:660

Module Section

Information Geometry of CES:

In the same file