binarySymmetricCapacity

formal source

  46    C = 1 - [-p log₂ p - (1-p) log₂ (1-p)]
  47
  48    Can transmit reliably at any rate R < C! -/
  49noncomputable def binarySymmetricCapacity (p : ℝ) : ℝ :=
  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! -/
  57noncomputable def capacity_at_10_percent : ℝ :=
  58  binarySymmetricCapacity 0.1
  59
  60/-! ## Error Correction Codes -/
  61
  62/-- An (n, k, d) code:
  63    - n = codeword length
  64    - k = message length
  65    - d = minimum distance
  66
  67    Can correct up to ⌊(d-1)/2⌋ errors.
  68    Rate R = k/n. -/
  69structure ErrorCode where
  70  n : ℕ  -- codeword length
  71  k : ℕ  -- message length
  72  d : ℕ  -- minimum distance
  73
  74/-- The Hamming bound (sphere-packing bound):
  75
  76    For t-error-correcting code:
  77    2^k × Σᵢ₌₀ᵗ C(n,i) ≤ 2ⁿ
  78
  79    Codes meeting this bound are "perfect" (e.g., Hamming codes).