def definition def or abbrev

`rateDistortionTheory`

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

formal statement (Lean)

 148def rateDistortionTheory : String :=

proof body

Definition body.

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

depends on (10)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
K in IndisputableMonolith.Constants decl_use
K in IndisputableMonolith.Constants.LambdaRecDerivation decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
that in IndisputableMonolith.NumberTheory.PhiLadderLattice decl_use