OAI/NumberTheory/TwoPoint/Walks/ColumnBudget.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual short-block budgets have the exponent required by the column code.

  1. lemma OAI.TwoPointCorrelations.eventually_short_block_floor line 12
  2. theorem OAI.TwoPointCorrelations.column_budget_bound line 24

    Source documentation

    The two-half allowance is the final +2 in the block count. All remaining constants are absolute, and the exponent is exactly 0.92.

    theorem column_budget_bound (L : ℝ) (hL : 1 ≤ L)
    (n s imperfect omittedLabels blocks segments omittedRuns : ℕ)
    (hn : (n : ℝ) ≤ 2 * L)
    (hs : L ^ (1 / 10 : ℝ) / 2 ≤ (s : ℝ))
    (hI : (imperfect : ℝ) ≤ 2 * L ^ (1 / 4 : ℝ))
    (hO : (omittedLabels : ℝ) ≤ 2 * L ^ (1 / 50 : ℝ))
    (hB : blocks ≤ n / s + imperfect + 2)
    (hS : segments ≤ (omittedLabels + 1) * blocks)
    (hR : omittedRuns ≤ omittedLabels * blocks) :
    ((2 * segments + omittedRuns + imperfect : ℕ) : ℝ) ≤ 66 * L ^ (0.92 : ℝ) := by
…