Documentation

Lean 4 Proof

theorem kl_reverse (z : ℝ) :
    klDivExp 1 (1 / z) = welfareDistanceFn (1 / z) := by
  simp only [klDivExp, welfareDistanceFn, one_div,
             div_one, Real.log_inv]
  ring

Dependency Graph

Location

thesis/CESProofs/Foundations/InformationGeometry.lean:112

Module Section

Information Geometry of CES:

In the same file