Sections / Section 6: Information Geometry and Cumulant Tower / fisherRao_distance_invariance

Coordinate invariance of natural gradient

theoremprovedInfo Geometrykey theorem

Documentation

Lean 4 Proof

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

Dependency Graph

Location

thesis/CESProofs/Foundations/InformationGeometry.lean:609

Module Section

Information Geometry of CES:

In the same file

bregmanDiv welfare_eq_bregman klDivExp welfare_eq_kl kl_reverse welfareDistanceFn_deriv welfareDistanceFn_second_deriv fisherInfoExp welfare_curvature_is_fisher hessLogFEigenvalue hessLogF_from_cesEigenvalue escortFisherEigenvalue bridgeRatio bridge_theorem curvatureK_eq_bridge_times_fisher curvatureK_from_hessLogF fifth_role_of_K hierarchical_kl bridgeRatio_pos bridgeRatio_large_at_small_rho