correction

formal source

  30
  31/-- The φ-ladder finite-N correction factor for quantum channel
  32capacity at input-symbol-count `N`. -/
  33def correction (N : ℕ) (hN : 0 < N) : ℝ := 1 / (phi * (N : ℝ))
  34
  35/-- Correction is strictly positive at every positive `N`. -/
  36theorem correction_pos (N : ℕ) (hN : 0 < N) : 0 < correction N hN := by
  37  unfold correction
  38  have hphi : 0 < phi := Constants.phi_pos
  39  have hNpos : (0 : ℝ) < (N : ℝ) := by exact_mod_cast hN
  40  positivity
  41
  42/-- Correction strictly decreases with `N` (from `N` to `N+1`). -/
  43theorem correction_strictly_decreasing (N : ℕ) (hN : 0 < N) :
  44    correction (N + 1) (Nat.succ_pos _) < correction N hN := by
  45  unfold correction
  46  have hphi : 0 < phi := Constants.phi_pos
  47  have hNpos : (0 : ℝ) < (N : ℝ) := by exact_mod_cast hN
  48  have hN1pos : (0 : ℝ) < ((N + 1 : ℕ) : ℝ) := by exact_mod_cast Nat.succ_pos _
  49  have hphiN_pos : (0 : ℝ) < phi * (N : ℝ) := by positivity
  50  have hphiN1_pos : (0 : ℝ) < phi * ((N + 1 : ℕ) : ℝ) := by positivity
  51  have hphi_le_strict : phi * (N : ℝ) < phi * ((N + 1 : ℕ) : ℝ) := by
  52    apply mul_lt_mul_of_pos_left ?_ hphi
  53    exact_mod_cast Nat.lt_succ_self N
  54  exact one_div_lt_one_div_of_lt hphiN_pos hphi_le_strict
  55
  56/-- Correction tends to 0 as `N → ∞` (statement form using single
  57positive `N`; the limit is the standard `1/N → 0`). -/
  58theorem correction_le_inv {N : ℕ} (hN : 0 < N) :
  59    correction N hN ≤ 1 / (N : ℝ) := by
  60  unfold correction
  61  have hphi_gt_one : (1 : ℝ) < phi := by
  62    have := Constants.phi_gt_onePointFive; linarith
  63  have hphi : 0 < phi := Constants.phi_pos