source_coding_theorem

formal source

  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
  73    H = -0.5 log₂(0.5) - 0.5 log₂(0.5) = 0.5 + 0.5 = 1 bit
  74
  75    Can't compress below 1 bit per symbol! -/
  76noncomputable def fairCoinEntropy : ℝ :=
  77  -0.5 * log2 0.5 - 0.5 * log2 0.5
  78
  79theorem fair_coin_one_bit :
  80    fairCoinEntropy = 1 := by
  81  unfold fairCoinEntropy
  82  simp only [show (0.5 : ℝ) = 1/2 from by norm_num]
  83  rw [log2_half]
  84  ring
  85
  86/-- Example: Biased coin (entropy < 1 bit).
  87
  88    P(H) = 0.9, P(T) = 0.1
  89    H = -0.9 log₂(0.9) - 0.1 log₂(0.1)
  90      ≈ 0.137 + 0.332 ≈ 0.47 bits