Documentation

Lean 4 Proof

theorem renyi_entropy_le_log_J {J : ℕ} (hJ : 0 < J) {α : ℝ}
    (hα₀ : 0 < α) (hα₁ : α ≠ 1) (p : Fin J → ℝ) (hp : ∀ j, 0 ≤ p j)
    (hsum : ∑ j : Fin J, p j = 1) :
    (1 / (1 - α)) * Real.log (∑ j : Fin J, (p j) ^ α) ≤ Real.log ↑J := by
  have hJr : (0 : ℝ) < ↑J := Nat.cast_pos.mpr hJ
  have hpos := power_sum_pos hJ hα₀ p hp hsum
  rcases lt_or_gt_of_ne hα₁ with hlt | hgt
  · -- Case α < 1: 1/(1-α) > 0, Σ p^α ≤ J^{1-α}
    have h1a : 0 < 1 - α := by linarith
    have hbound := power_sum_bound_concave hJ hα₀ (le_of_lt hlt) p hp hsum
    have hlog := Real.log_le_log hpos hbound
    rw [Real.log_rpow hJr] at hlog
    -- hlog : log(Σ p^α) ≤ (1-α) * log J
    rw [one_div]
    calc (1 - α)⁻¹ * Real.log (∑ j, (p j) ^ α)
        ≤ (1 - α)⁻¹ * ((1 - α) * Real.log ↑J) :=
          mul_le_mul_of_nonneg_left hlog (le_of_lt (inv_pos.mpr h1a))
      _ = Real.log ↑J := by
          rw [← mul_assoc, inv_mul_cancel₀ (ne_of_gt h1a), one_mul]
  · -- Case α > 1: 1/(1-α) < 0, Σ p^α ≥ J^{1-α}
    have h1a : 1 - α < 0 := by linarith
    have hbound := power_sum_bound_convex hJ (le_of_lt hgt) p hp hsum
    have hlog := Real.log_le_log (rpow_pos_of_pos hJr _) hbound
    rw [Real.log_rpow hJr] at hlog
    -- hlog : (1-α) * log J ≤ log(Σ p^α)
    rw [one_div]
    calc (1 - α)⁻¹ * Real.log (∑ j, (p j) ^ α)
        ≤ (1 - α)⁻¹ * ((1 - α) * Real.log ↑J) :=
          mul_le_mul_of_nonpos_left hlog (le_of_lt (inv_lt_zero.mpr h1a))
      _ = Real.log ↑J := by
          rw [← mul_assoc, inv_mul_cancel₀ (ne_of_lt h1a), one_mul]

Dependency Graph

Location

thesis/CESProofs/Foundations/Emergence.lean:369

Module Section

Emergence results from Paper 1, Sections 3-5:

In the same file