Documentation

Lean 4 Proof

def alphaDivergence (α : ℝ) (p q : Fin J → ℝ) : ℝ :=
  4 / (1 - α ^ 2) * (1 - ∑ j : Fin J,
    p j ^ ((1 + α) / 2) * q j ^ ((1 - α) / 2))

Dependency Graph

Location

thesis/CESProofs/Foundations/TripleCorrespondence.lean:255

Module Section

### Market Equilibrium as Information Projection

In the same file