pith. machine review for the scientific record. sign in
theorem proved term proof

shannon_equals_jcost

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 149theorem shannon_equals_jcost {n : ℕ} (d : ProbDist n) :
 150    shannonEntropy d = totalJCost d := by

proof body

Term-mode proof.

 151  -- Both compute Σ p_i × (-log p_i), just with different notation
 152  -- shannonEntropy = -(Σ p*log(p)) and totalJCost = Σ p*(-log(p))
 153  -- These are equal since -(p*log(p)) = p*(-log(p))
 154  unfold shannonEntropy totalJCost probJCost
 155  -- Goal: -(Σ if p>0 then p*log(p) else 0) = Σ if p>0 then p*(-log(p)) else 0
 156  conv_lhs =>
 157    rw [← Finset.sum_neg_distrib]
 158  congr 1
 159  funext i
 160  by_cases hp : d.probs i > 0
 161  · simp only [hp, ↓reduceIte, dite_eq_ite, neg_mul, mul_neg, neg_neg]
 162  · simp only [hp, ↓reduceIte, dite_eq_ite, neg_zero]
 163
 164/-! ## Information Content -/
 165
 166/-- Information content (surprisal) of an outcome.
 167    I(x) = -log(p(x)) = "how surprising is this outcome?" -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (18)

Lean names referenced from this declaration's body.