Prove2Me

Asymptotic volume of the strict row simplex

Proved
OAI.PiExponent.DeterminantContradiction.row_count_asymptotic

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

number-theoryopenai-pi-exponent-017

For admissible fixed data, the row count divided by H^(m+1) converges to K times the volume coefficient of its strict weighted simplex.

Preamble
import Definitions.Def_OAI_NumberTheory_PiExponent_Analysis_AnalyticAggregate_RemainderData

open scoped BigOperators Topology
open Filter
open OAI.PiExponent OAI.PiExponent.DeterminantContradiction
open OAI.PiExponent.LiteralAnalytic
Formal statement
theorem OAI.PiExponent.DeterminantContradiction.row_count_asymptotic
    {nu : ℝ} (d : FixedData nu) :
    Tendsto
      (fun H : ℝ => (actualRowCount d H : ℝ) / H ^ (d.m + 1))
      atTop
      (𝓝 (((d.K : ℝ) * (d.base.theta : ℝ) ^ d.m) /
        ((Nat.factorial (d.m + 1) : ℝ) * (d.v0 : ℝ) *
          ∏ i : Fin d.m, d.x (i.val + 1)))) := by sorry
Source
https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/NumberTheory/PiExponent/Analysis/LiteralAnalyticSummand.lean#L177-L199

View graph