gapAt_pos

formal source

  28/-- Gap-to-capacity at φ-ladder rung `k`. -/
  29def gapAt (k : ℕ) : ℝ := referenceGap * phi ^ (-(k : ℤ))
  30
  31theorem gapAt_pos (k : ℕ) : 0 < gapAt k := by
  32  unfold gapAt referenceGap
  33  have : 0 < phi ^ (-(k : ℤ)) := zpow_pos Constants.phi_pos _
  34  linarith [this]
  35
  36theorem gapAt_succ_ratio (k : ℕ) :
  37    gapAt (k + 1) = gapAt k * phi⁻¹ := by
  38  unfold gapAt
  39  have hphi_ne : phi ≠ 0 := Constants.phi_ne_zero
  40  have : phi ^ (-((k : ℤ) + 1)) = phi ^ (-(k : ℤ)) * phi⁻¹ := by
  41    rw [show (-((k : ℤ) + 1)) = -(k : ℤ) + (-1 : ℤ) by ring]
  42    rw [zpow_add₀ hphi_ne]; simp
  43  have hcast : ((k + 1 : ℕ) : ℤ) = (k : ℤ) + 1 := by push_cast; ring
  44  rw [hcast, this]; ring
  45
  46theorem gapAt_adjacent_ratio (k : ℕ) :
  47    gapAt (k + 1) / gapAt k = phi⁻¹ := by
  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