pith. machine review for the scientific record. sign in
def definition def or abbrev

messageJCost

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

 117noncomputable def messageJCost (length redundancy : ℝ) : ℝ :=

proof body

Definition body.

 118  length * (1 - redundancy)
 119
 120/-! ## Lossless vs Lossy Compression -/
 121
 122/-- Lossless compression:
 123    - Exact reconstruction possible
 124    - Limit: H(X) bits
 125    - Examples: ZIP, PNG, FLAC
 126
 127    In RS: Preserves all ledger information -/

depends on (7)

Lean names referenced from this declaration's body.