OAI/NumberTheory/TwoPoint/Walks/ForestCodeAsymptotics.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Absorbing the sublinear endpoint and exceptional-position costs.

  1. lemma OAI.TwoPointCorrelations.eventually_sublinear_log_cost line 12
  2. lemma OAI.TwoPointCorrelations.eventually_forest_endpoint_cost line 32
  3. theorem OAI.TwoPointCorrelations.eventually_column_code_exponential line 49

    Source documentation

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

    theorem eventually_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 →
      ((2 * segments + omitted + imperfect : ℕ) : ℝ) ≤ C * L ^ (0.92 : ℝ) →
      (Fintype.card (ColumnCode N segments omitted imperfect) : ℝ) ≤
        Real.exp (44 * k) := by
…

    Mentions: OAI.TwoPointCorrelations.ColumnCode