module module

`IndisputableMonolith.Information.ShannonEntropy`

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

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Information.Compression module_import
IndisputableMonolith.Information.ErrorCorrectionBounds module_import
IndisputableMonolith.Information.InformationIsLedger module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (19)

structure ProbDist L48
def uniform L57
def shannonEntropy L67
theorem entropy_nonneg L73
theorem max_entropy_uniform L92
theorem zero_entropy_deterministic L111
def probJCost L126
theorem jcost_uniform L131
def totalJCost L137
theorem shannon_equals_jcost L149
def surprisal L168
theorem entropy_is_expected_surprisal L171
theorem entropy_from_recognition_cost L192
theorem source_coding_theorem L200
def entropyApplications L210
def boltzmannFactor L220
theorem thermodynamic_entropy_connection L222
structure ShannonFalsifier L232
def experimentalStatus L239