Documentation

Lean 4 Proof

theorem bhattacharyya_uniform_self {J : ℕ} (hJ : 0 < J) :
    bhattacharyyaCoeff (symmetricShare J) (symmetricShare J) = 1 :=
  fisherRaoDistance_self (symmetricShare J)
    (fun _ => by simp [symmetricShare])
    (symmetricShare_sum hJ)

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/InformationGeometry.lean:461

Module Section

Information Geometry of CES:

In the same file