Documentation

Lean 4 Proof

def effectiveCESPotential (J : ℕ) (q T : ℝ) (p : Fin J → ℝ) (ε : Fin J → ℝ) : ℝ :=
  ∑ j : Fin J, p j * ε j -
  T * (if q = 1 then -∑ j : Fin J, p j * Real.log (p j)
       else (1 - ∑ j : Fin J, (p j) ^ q) / (q - 1))

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/AggregationInvariantClass.lean:90

Module Section

Aggregation-invariant class results from Paper 1, Section 5:

In the same file