Documentation

Lean 4 Proof

theorem welfare_eq_bregman (z : ℝ) :
    welfareDistanceFn z =
    bregmanDiv (-Real.log z) (-Real.log 1) (-1) z 1 := by
  simp only [welfareDistanceFn, bregmanDiv, Real.log_one, neg_zero]
  ring

Dependency Graph

Location

thesis/CESProofs/Foundations/InformationGeometry.lean:67

Module Section

Information Geometry of CES:

In the same file