module
module
IndisputableMonolith.Holography.RecognitionEventCapacity
show as:
view Lean formalization →
used by (1)
depends on (1)
declarations in this module (13)
-
def
forcedEntropy -
theorem
one_sub_rho_eq_sq -
theorem
probMass_eq_inv_pow -
theorem
neglog_probMass -
theorem
forcedEntropy_eq -
def
effectiveOutcomes -
theorem
effectiveOutcomes_eq -
def
bitsPerEvent -
theorem
bitsPerEvent_eq -
def
eventAccess -
theorem
eventAccess_additive -
structure
EventCapacityCert -
theorem
eventCapacityCert