Documentation

Lean 4 Proof

theorem welfare_eq_kl {z : ℝ} (_hz : 0 < z) :
    welfareDistanceFn z = klDivExp (1 / z) 1 := by
  simp only [welfareDistanceFn, klDivExp, div_one, one_div,
             Real.log_inv, inv_inv]
  ring

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/InformationGeometry.lean:104

Module Section

Information Geometry of CES:

In the same file