Documentation

Lean 4 Proof

theorem collision_entropy_le_log_J {J : ℕ} (hJ : 0 < J) (p : Fin J → ℝ)
    (hsum : ∑ j : Fin J, p j = 1) (_hp : ∀ j, 0 ≤ p j) :
    -Real.log (∑ j : Fin J, (p j) ^ 2) ≤ Real.log ↑J := by
  have hJr : (0 : ℝ) < ↑J := Nat.cast_pos.mpr hJ
  have hsq := sum_sq_ge_inv_card hJ p hsum
  have hsp : 0 < ∑ j : Fin J, (p j) ^ 2 := lt_of_lt_of_le (div_pos one_pos hJr) hsq
  rw [neg_le, ← Real.log_inv]
  apply Real.log_le_log (inv_pos.mpr hJr)
  rwa [one_div] at hsq

Dependency Graph

Location

thesis/CESProofs/Foundations/Emergence.lean:266

Module Section

Emergence results from Paper 1, Sections 3-5:

In the same file