Documentation

Lean 4 Proof

theorem management_return_sign (J : ℕ) (q _T : ℝ) (p : Fin J → ℝ)
    (hp : OnOpenSimplex J p) (hq : 0 < q) :
    0 ≤ tsallisEntropy J q p :=
  tsallis_nonneg J q p hp hq

Dependency Graph

Location

thesis/CESProofs/Potential/Welfare.lean:79

Module Section

Theorem 8, Corollary 6, Propositions 18-22:

In the same file