Documentation

Lean 4 Proof

theorem sum_sq_ge_inv_card {J : ℕ} (hJ : 0 < J) (p : Fin J → ℝ)
    (hsum : ∑ j : Fin J, p j = 1) :
    1 / (↑J : ℝ) ≤ ∑ j : Fin J, (p j) ^ 2 := by
  have hJr : (0 : ℝ) < ↑J := Nat.cast_pos.mpr hJ
  rw [div_le_iff₀ hJr]
  -- Goal: 1 ≤ ↑J * Σ p_j²
  calc (1 : ℝ) = (∑ j : Fin J, p j) ^ 2 := by rw [hsum]; ring
    _ = (∑ j : Fin J, p j * 1) ^ 2 := by simp
    _ ≤ (∑ j : Fin J, (p j) ^ 2) * (∑ j : Fin J, (1 : ℝ) ^ 2) :=
        Finset.sum_mul_sq_le_sq_mul_sq Finset.univ _ _
    _ = (∑ j : Fin J, (p j) ^ 2) * ↑J := by
        simp [Finset.sum_const, nsmul_eq_mul]

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/Emergence.lean:252

Module Section

Emergence results from Paper 1, Sections 3-5:

In the same file