`losslessCompression`

definition

show as: view math explainer →

module: IndisputableMonolith.Information.Compression
domain: Information
line: 128 · 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 128.

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

 125    - Examples: ZIP, PNG, FLAC
 126
 127    In RS: Preserves all ledger information -/
 128def losslessCompression : String :=
 129  "Exact reconstruction, limit = entropy"
 130
 131/-- Lossy compression:
 132    - Approximate reconstruction
 133    - Can go below H(X) with distortion
 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

papers checked against this theorem

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