pith. machine review for the scientific record. sign in
def definition def or abbrev

lempelZiv

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)

 199def lempelZiv : String :=

proof body

Definition body.

 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) -/

depends on (6)

Lean names referenced from this declaration's body.