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

Kl Div Exp

defprovedInfo Geometry

Documentation

Lean 4 Proof

def klDivExp (rate1 rate2 : ℝ) : ℝ :=
  Real.log (rate1 / rate2) - 1 + rate2 / rate1

Dependency Graph

Used by

kl_reverse hierarchical_kl welfare_eq_kl

Location

thesis/CESProofs/Foundations/InformationGeometry.lean:84

Module Section

Information Geometry of CES:

In the same file

bregmanDiv welfare_eq_bregman 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 bridgeRatio_at_one