A coordinate-box bound for the actual row count
ProvedOAI.PiExponent.DeterminantContradiction.actualRowCount_real_boundnumber-theoryopenai-pi-exponent-017
For nonnegative H, the actual row count is bounded by the number of points in a coordinate box: K choices for the finite factor, at most H/v0+1 choices in the distinguished coordinate, and at most H+1 choices in each of the remaining m coordinates.
Preamble
import Definitions.Def_OAI_NumberTheory_PiExponent_Analysis_AnalyticAggregate_RemainderData open scoped BigOperators Topology open OAI.PiExponent OAI.PiExponent.DeterminantContradiction
Formal statement
theorem OAI.PiExponent.DeterminantContradiction.actualRowCount_real_bound {nu : ℝ} (d : OAI.PiExponent.DeterminantContradiction.FixedData nu) (H : ℝ) (hH : 0 ≤ H) : (OAI.PiExponent.DeterminantContradiction.actualRowCount d H : ℝ) ≤ (d.K : ℝ) * (H / (d.v0 : ℝ) + 1) * (H + 1) ^ d.m := by sorrySource