gap_pos

formal source

  50/-- Gap to Shannon capacity for an LDPC code of block length N. -/
  51def gapToCapacity (N : ℝ) : ℝ := 1 / (phi * N)
  52
  53theorem gap_pos {N : ℝ} (hN : 0 < N) : 0 < gapToCapacity N := by
  54  unfold gapToCapacity
  55  apply one_div_pos.mpr
  56  exact mul_pos phi_pos hN
  57
  58theorem gap_decreasing {N₁ N₂ : ℝ} (h₁ : 0 < N₁) (h_lt : N₁ < N₂) :
  59    gapToCapacity N₂ < gapToCapacity N₁ := by
  60  unfold gapToCapacity
  61  have h₂ : 0 < N₂ := lt_trans h₁ h_lt
  62  have hp : 0 < phi := phi_pos
  63  have hphi_N1 : 0 < phi * N₁ := mul_pos hp h₁
  64  have hphi_N2 : 0 < phi * N₂ := mul_pos hp h₂
  65  -- 1 / (phi * N₂) < 1 / (phi * N₁) since phi * N₁ < phi * N₂
  66  have h_lt' : phi * N₁ < phi * N₂ := mul_lt_mul_of_pos_left h_lt hp
  67  exact one_div_lt_one_div_of_lt hphi_N1 h_lt'
  68
  69/-- Doubling N halves the gap. -/
  70theorem gap_doubling_halves {N : ℝ} (hN : 0 < N) :
  71    gapToCapacity (2 * N) = gapToCapacity N / 2 := by
  72  unfold gapToCapacity
  73  have hp : phi ≠ 0 := phi_ne_zero
  74  have hN' : N ≠ 0 := ne_of_gt hN
  75  field_simp
  76
  77/-- For N = 10000, the gap matches the empirical ~0.5 dB ≈ 1/(φ·10⁴). -/
  78def gapAt10k : ℝ := gapToCapacity 10000
  79
  80theorem gap_at_10k_eq : gapAt10k = 1 / (phi * 10000) := rfl
  81
  82theorem gap_at_10k_pos : 0 < gapAt10k := by
  83  unfold gapAt10k; exact gap_pos (by norm_num : (0:ℝ) < 10000)