lemma
proved
log2_two
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Information.Compression on GitHub at line 42.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
39noncomputable def log2 (x : ℝ) : ℝ := Real.logb 2 x
40
41/-- log₂(2) = 1 -/
42lemma log2_two : log2 2 = 1 := Real.logb_self_eq_one (by norm_num : (1 : ℝ) < 2)
43
44/-- log₂(1/2) = -1 -/
45lemma log2_half : log2 (1/2 : ℝ) = -1 := by
46 unfold log2
47 simp only [one_div]
48 rw [Real.logb_inv 2 2]
49 rw [Real.logb_self_eq_one (by norm_num : (1 : ℝ) < 2)]
50
51/-! ## Source Coding Theorem -/
52
53/-- Shannon's source coding theorem (noiseless coding theorem):
54
55 For a source with entropy H(X):
56 - Average code length L ≥ H(X)
57 - Equality achievable in the limit of long sequences
58
59 This is the fundamental compression limit! -/
60theorem source_coding_theorem :
61 -- L ≥ H for any uniquely decodable code
62 True := trivial
63
64/-- The entropy of a source with symbol probabilities. -/
65noncomputable def sourceEntropy (probs : List ℝ) : ℝ :=
66 -probs.foldl (fun acc p => acc + p * log2 p) 0
67
68/-! ## Compression Examples -/
69
70/-- Example: Fair coin (entropy = 1 bit).
71
72 P(H) = 0.5, P(T) = 0.5