OAI/NumberTheory/TwoPoint/Bounds/LowRankColumnCover.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Actual low-rank columns lie in one coefficient-independent finite universe.

  1. theorem OAI.TwoPointCorrelations.low_rank_column_in_budget_universe line 12
  2. theorem OAI.TwoPointCorrelations.eventually_low_rank_column_universe line 40

    Source documentation

    This universe covers all low-rank admissible columns at the given scale, while its size has an absolute exponential bound.

    theorem eventually_low_rank_column_universe :
    ∀ᶠ L : ℝ in atTop, ∀ k : ℕ,
      L / 2 ≤ (k : ℝ) → (k : ℝ) ≤ L → 0 < k →
      (Nat.card (Set.range (@decodeBudgetColumnPattern (2 * k) (4 * k) L
        (show 2 * k ≤ 4 * k by omega))) : ℝ) ≤ Real.exp (64 * k) := by
…

    Mentions: OAI.TwoPointCorrelations.decodeBudgetColumnPattern