Prove2Me

An eventual polynomial bound for the row count

Proved
OAI.PiExponent.LiteralAnalytic.actualRowCount_eventually_polynomial_bound

by Eyal1990 · Oct 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

number-theoryopenai-pi-exponent-017

For fixed admissible data, at all sufficiently large cutoffs H the row count is at least one and is bounded above by a fixed positive constant times H to the power d.m + 1.

Preamble
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Mathlib.Analysis.SpecificLimits.Basic
import Mathlib.Analysis.SpecificLimits.Normed
import Definitions.Def_OAI_NumberTheory_PiExponent_Analysis_AnalyticAggregate_RemainderData

open scoped BigOperators Topology
open Filter
open OAI.PiExponent OAI.PiExponent.DeterminantContradiction OAI.PiExponent.LiteralAnalytic
Formal statement
theorem OAI.PiExponent.LiteralAnalytic.actualRowCount_eventually_polynomial_bound
    {nu : ℝ} (d : FixedData nu) :
    ∃ C : ℝ, 0 < C ∧ ∀ᶠ H : ℝ in atTop,
      0 < H ∧ 1 ≤ actualRowCount d H ∧
        (actualRowCount d H : ℝ) ≤ C * H ^ (d.m + 1 : ℕ) := by sorry
Source
https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/NumberTheory/PiExponent/Analysis/AnalyticAggregate.lean#L74-L94

View graph