Documentation

Lean 4 Proof

theorem fisherRaoDistance_self {J : ℕ} (s : Fin J → ℝ)
    (hs : ∀ j, 0 ≤ s j)
    (hsum : ∑ j : Fin J, s j = 1) :
    bhattacharyyaCoeff s s = 1 := by
  simp only [bhattacharyyaCoeff]
  simp_rw [Real.sqrt_mul_self (hs _)]
  exact hsum

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/InformationGeometry.lean:433

Module Section

Information Geometry of CES:

In the same file