  48  rw [gapAt_succ_ratio]
  49  field_simp [(gapAt_pos k).ne']
  50
  51structure PolarCodeCert where
  52  gap_pos : ∀ k, 0 < gapAt k
  53  one_step_ratio : ∀ k, gapAt (k + 1) = gapAt k * phi⁻¹
  54  adjacent_ratio : ∀ k, gapAt (k + 1) / gapAt k = phi⁻¹
  55
  56/-- Polar-code gap-to-capacity certificate. -/
  57def polarCodeCert : PolarCodeCert where
  58  gap_pos := gapAt_pos
  59  one_step_ratio := gapAt_succ_ratio
  60  adjacent_ratio := gapAt_adjacent_ratio
  61
  62end
  63end PolarCodeGapFromPhi
  64end Information
  65end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.