Documentation

Lean 4 Proof

private theorem power_sum_pos {J : ℕ} (_hJ : 0 < J) {α : ℝ} (_hα : 0 < α)
    (p : Fin J → ℝ) (hp : ∀ j, 0 ≤ p j) (hsum : ∑ j : Fin J, p j = 1) :
    0 < ∑ j : Fin J, (p j) ^ α := by
  have ⟨j, hpj⟩ : ∃ j, 0 < p j := by
    by_contra h
    push_neg at h
    have : ∑ j : Fin J, p j ≤ 0 :=
      Finset.sum_nonpos fun j _ => le_antisymm (h j) (hp j) ▸ le_refl _
    linarith
  calc 0 < (p j) ^ α := rpow_pos_of_pos hpj α
    _ ≤ ∑ i : Fin J, (p i) ^ α :=
        Finset.single_le_sum (fun i _ => rpow_nonneg (hp i) α) (Finset.mem_univ j)

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/Emergence.lean:350

Module Section

Emergence results from Paper 1, Sections 3-5:

In the same file