def
definition
lossyCompression
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 137.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
134 - Examples: JPEG, MP3, video codecs
135
136 In RS: Discards high J-cost (less important) information -/
137def lossyCompression : String :=
138 "Approximate reconstruction, accepts distortion"
139
140/-- Rate-distortion theory:
141
142 R(D) = minimum rate for distortion ≤ D
143
144 Trade-off between compression and quality.
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!