`huffmanCoding`

definition

show as: view math explainer →

module: IndisputableMonolith.Information.Compression
domain: Information
line: 184 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Information.Compression on GitHub at line 184.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 181    - Optimal for symbol-by-symbol coding
 182    - L ≤ H + 1 (within 1 bit of entropy)
 183    - Uses shorter codes for common symbols -/
 184def huffmanCoding : String :=
 185  "Optimal prefix-free code, L ≤ H + 1"
 186
 187/-- Arithmetic coding:
 188    - Near-optimal for any distribution
 189    - L → H as message length → ∞
 190    - Encodes message as a single number -/
 191def arithmeticCoding : String :=
 192  "Near-optimal, L → H for long messages"
 193
 194/-- Lempel-Ziv compression (LZ77, LZ78, LZW):
 195    - Dictionary-based
 196    - Adaptive (learns patterns)
 197    - Achieves entropy in limit
 198    - Used in ZIP, PNG, GIF -/
 199def lempelZiv : String :=
 200  "Dictionary-based, adaptive, asymptotically optimal"
 201
 202/-! ## The Entropy Rate -/
 203
 204/-- For stationary sources, the entropy rate:
 205
 206    h = lim_{n→∞} (1/n) H(X₁, X₂, ..., Xₙ)
 207
 208    This accounts for correlations between symbols.
 209
 210    Example: English text
 211    - Single letter entropy: ~4.2 bits/letter
 212    - Entropy rate: ~1.0-1.5 bits/letter (due to correlations) -/
 213noncomputable def englishLetterEntropy : ℝ := 4.2  -- bits
 214noncomputable def englishEntropyRate : ℝ := 1.2  -- bits

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.