BoundedColumnCodes.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

One code universe when segment, omitted-run and imperfect counts vary.

abbrev OAI.TwoPointCorrelations.BoundedColumnDecoderCode line 11

theorem OAI.TwoPointCorrelations.card_boundedColumnDecoderCode_le line 17

Source documentation

Taking the union over the permitted counts costs only three polynomial factors. It does not impose common counts on different realizations.

theorem card_boundedColumnDecoderCode_le (N segments omitted imperfect : ℕ) (hN : 1 ≤ N) :
    Fintype.card (BoundedColumnDecoderCode N segments omitted imperfect) ≤
      ((segments + 1) * (omitted + 1) * (imperfect + 1)) *
        (2 ^ (6 * N + 1) * N ^ (2 * segments + omitted + imperfect)) := by
…

Mentions: OAI.TwoPointCorrelations.BoundedColumnDecoderCode

def OAI.TwoPointCorrelations.decodeBoundedColumnPattern line 36

theorem OAI.TwoPointCorrelations.card_bounded_column_patterns line 42

Source documentation

This is the full coefficient-independent image, including all permitted segment and exceptional-position counts.

theorem card_bounded_column_patterns (N segments omitted imperfect : ℕ) (hN : 1 ≤ N) :
    Nat.card (Set.range (@decodeBoundedColumnPattern N segments omitted imperfect)) ≤
      ((segments + 1) * (omitted + 1) * (imperfect + 1)) *
        (2 ^ (6 * N + 1) * N ^ (2 * segments + omitted + imperfect)) := by
…

Mentions: OAI.TwoPointCorrelations.decodeBoundedColumnPattern

theorem OAI.TwoPointCorrelations.eventually_bounded_column_code_exponential line 56

Source documentation

The union over all bounded counts still has an absolute exponential cost. Fixed constants in the sublinear budget affect only the threshold.

theorem eventually_bounded_column_code_exponential (C : ℝ) (hC : 0 ≤ C) :
    ∀ᶠ L : ℝ in atTop, ∀ k N segments omitted imperfect : ℕ,
      L / 2 ≤ (k : ℝ) → (k : ℝ) ≤ L → 1 ≤ N → N ≤ 4 * k →
      segments ≤ N → omitted ≤ N → imperfect ≤ N →
      ((2 * segments + omitted + imperfect : ℕ) : ℝ) ≤ C * L ^ (0.92 : ℝ) →
      (Fintype.card (BoundedColumnDecoderCode N segments omitted imperfect) : ℝ) ≤
        Real.exp (64 * k) := by
…

Mentions: OAI.TwoPointCorrelations.BoundedColumnDecoderCode