Documentation

Lean 4 Proof

theorem hierarchical_kl {N : ℕ} (z : Fin N → ℝ) (hz : ∀ n, 0 < z n)
    (treeCoeff : Fin N → ℝ) :
    ∑ n : Fin N, treeCoeff n * welfareDistanceFn (z n) =
    ∑ n : Fin N, treeCoeff n * klDivExp (1 / z n) 1 := by
  congr 1; ext n
  rw [welfare_eq_kl (hz n)]

Dependency Graph

Location

thesis/CESProofs/Foundations/InformationGeometry.lean:355

Module Section

Information Geometry of CES:

In the same file