def definition def or abbrev

`binarySymmetricCapacity`

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

formal statement (Lean)

  49noncomputable def binarySymmetricCapacity (p : ℝ) : ℝ :=

proof body

Definition body.

  50  1 + p * (Real.log p / Real.log 2) + (1-p) * (Real.log (1-p) / Real.log 2)
  51
  52/-- For p = 0.1 (10% error rate):
  53    H(0.1) ≈ 0.47 bits
  54    C ≈ 0.53 bits per channel use
  55
  56    Can still transmit reliably at 53% of raw capacity! -/

used by (1)

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

capacity_at_10_percent in IndisputableMonolith.Information.ErrorCorrectionBounds decl_use

depends on (7)

Lean names referenced from this declaration's body.

H in IndisputableMonolith.Algebra.CostAlgebra decl_use
of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
H in IndisputableMonolith.Cost.FunctionalEquation decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use