Documentation

Lean 4 Proof

theorem tsallis_nonneg (J : ℕ) (q : ℝ) (p : Fin J → ℝ)
    (hp : OnOpenSimplex J p) (_hq : 0 < q) :
    0 ≤ tsallisEntropy J q p := by
  unfold tsallisEntropy
  split_ifs with h
  · -- q = 1: Shannon entropy -Σ p log p ≥ 0
    rw [neg_nonneg]
    apply Finset.sum_nonpos
    intro j _
    exact mul_nonpos_of_nonneg_of_nonpos (le_of_lt (hp.1 j))
      (Real.log_nonpos (le_of_lt (hp.1 j)) (simplex_component_le_one hp j))
  · -- q ≠ 1: (1 - Σ p^q)/(q-1)
    apply div_nonneg_iff.mpr
    rcases lt_or_gt_of_ne h with hq1 | hq1
    · -- q < 1: Σ p^q ≥ 1 (each p^q ≥ p) and q-1 < 0
      right
      constructor
      · have : 1 ≤ ∑ j : Fin J, (p j) ^ q := by
          rw [← hp.2]
          apply Finset.sum_le_sum
          intro j _
          have : (p j) ^ (1 : ℝ) ≤ (p j) ^ q :=
            Real.rpow_le_rpow_of_exponent_ge (hp.1 j) (simplex_component_le_one hp j)
              (le_of_lt hq1)
          simpa using this
        linarith
      · linarith
    · -- q > 1: Σ p^q ≤ 1 (each p^q ≤ p) and q-1 > 0
      left
      constructor
      · have : ∑ j : Fin J, (p j) ^ q ≤ 1 := by
          rw [← hp.2]
          apply Finset.sum_le_sum
          intro j _
          have : (p j) ^ q ≤ (p j) ^ (1 : ℝ) :=
            Real.rpow_le_rpow_of_exponent_ge (hp.1 j) (simplex_component_le_one hp j)
              (le_of_lt hq1)
          simpa using this
        linarith
      · linarith

Dependency Graph

Used by

Location

thesis/CESProofs/Potential/Welfare.lean:31

Module Section

Theorem 8, Corollary 6, Propositions 18-22:

In the same file