def definition def or abbrev

`losslessCompression`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 128def losslessCompression : String :=

proof body

Definition body.

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

depends on (7)

Lean names referenced from this declaration's body.

H in IndisputableMonolith.Algebra.CostAlgebra decl_use
H in IndisputableMonolith.Cost.FunctionalEquation decl_use
entropy in IndisputableMonolith.Foundation.InitialCondition decl_use
cost in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4 decl_use
cost in IndisputableMonolith.Foundation.ObserverForcing decl_use
entropy in IndisputableMonolith.Thermodynamics.BoltzmannDistribution decl_use
entropy in IndisputableMonolith.Thermodynamics.PartitionFunction decl_use