def definition def or abbrev

`lossyCompression`

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

formal statement (Lean)

 137def lossyCompression : String :=

proof body

Definition body.

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

depends on (4)

Lean names referenced from this declaration's body.

cost in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4 decl_use
cost in IndisputableMonolith.Foundation.ObserverForcing decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use