ColumnDecoderAsymptotics.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Exponential bound for the universal full-column decoder.

theorem OAI.TwoPointCorrelations.eventually_column_decoder_exponential line 14

Source documentation

The exponent constant is absolute. Fixed coefficients in the sublinear segment budget only change the lower threshold for L.

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

Mentions: OAI.TwoPointCorrelations.ColumnDecoderCode