def
definition
rateDistortionTheory
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Information.Compression on GitHub at line 148.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
145
146 In RS: Which ledger information to discard
147 based on J-cost importance. -/
148def rateDistortionTheory : String :=
149 "Trade-off between compression rate and distortion"
150
151/-! ## Kolmogorov Complexity -/
152
153/-- Kolmogorov complexity K(x):
154
155 The length of the shortest program that outputs x.
156
157 K(x) ≤ length(x) + O(1) (can always use literal)
158 K(x) ≈ 0 for simple patterns
159 K(x) ≈ length(x) for random strings
160
161 In RS: K(x) = minimum ledger description of x -/
162def kolmogorovComplexity : String :=
163 "Shortest program length to output x"
164
165/-- Incompressibility:
166
167 Most strings are incompressible!
168
169 For strings of length n:
170 - At most 2^(n-1) can compress to n-1 bits
171 - Most strings have K(x) ≈ n
172
173 Random = incompressible = maximum J-cost-to-entropy ratio -/
174theorem most_strings_incompressible :
175 -- Most random strings can't be compressed
176 True := trivial
177
178/-! ## Practical Compression Algorithms -/