Documentation

Lean 4 Proof

theorem power_sum_bound_convex {J : ℕ} (hJ : 0 < J) {α : ℝ}
    (hα₁ : 1 ≤ α) (p : Fin J → ℝ) (hp : ∀ j, 0 ≤ p j)
    (hsum : ∑ j : Fin J, p j = 1) :
    (↑J : ℝ) ^ (1 - α) ≤ ∑ j : Fin J, (p j) ^ α := by
  have hJr : (0 : ℝ) < ↑J := Nat.cast_pos.mpr hJ
  have hJne : (↑J : ℝ) ≠ 0 := ne_of_gt hJr
  have hconv := convexOn_rpow hα₁
  set w : Fin J → ℝ := fun _ => (1 : ℝ) / ↑J
  have hw_nn : ∀ j ∈ Finset.univ, 0 ≤ w j := fun _ _ => by positivity
  have hw_sum : ∑ j ∈ Finset.univ, w j = 1 := by
    simp [w, Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
    exact div_self hJne
  have hx_mem : ∀ j ∈ Finset.univ, p j ∈ Set.Ici (0 : ℝ) :=
    fun j _ => Set.mem_Ici.mpr (hp j)
  -- Jensen (convex): f(Σ w·x) ≤ Σ w·f(x), so (1/J)^α ≤ (1/J)·Σ p^α
  have step := ConvexOn.map_sum_le hconv hw_nn hw_sum hx_mem
  simp only [smul_eq_mul, w] at step
  rw [← Finset.mul_sum, ← Finset.mul_sum, hsum, mul_one] at step
  -- Multiply by J: J^{1-α} = J·(1/J)^α ≤ J·(1/J)·Σ p^α = Σ p^α
  have halg : (↑J : ℝ) * (1 / ↑J : ℝ) ^ α = (↑J : ℝ) ^ (1 - α) := by
    conv_lhs => rw [show (↑J : ℝ) = (↑J : ℝ) ^ (1 : ℝ) from (rpow_one _).symm]
    rw [one_div, ← rpow_neg (le_of_lt hJr), ← rpow_mul (le_of_lt hJr),
        ← rpow_add hJr]
    congr 1; ring
  calc (↑J : ℝ) ^ (1 - α)
      = ↑J * (1 / ↑J) ^ α := halg.symm
    _ ≤ ↑J * ((1 / ↑J) * ∑ j : Fin J, (p j) ^ α) :=
        mul_le_mul_of_nonneg_left step (le_of_lt hJr)
    _ = ∑ j : Fin J, (p j) ^ α := by field_simp

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/Emergence.lean:319

Module Section

Emergence results from Paper 1, Sections 3-5:

In the same file