Explicit polynomial bound for the coordinate box product
ProvedOAI.PiExponent.DeterminantContradiction.weightedStrictSimplex_box_product_bound_explicitnumber-theoryopenai-pi-exponent-017
For fixed positive weights, the coordinate box product is eventually bounded by the explicit constant product of (2 + 1 / w i) times (H + 1) to the number of coordinates.
Preamble
import Definitions.Def_OAI_NumberTheory_PiExponent_Approximation_InterpolationMatrix_Domains import Definitions.Def_OAI_NumberTheory_PiExponent_Polynomials_SimplexCounting_WeightedDomains open Filter open scoped Topology BigOperators
Formal statement
theorem OAI.PiExponent.DeterminantContradiction.weightedStrictSimplex_box_product_bound_explicit
{m : ℕ} (w : Fin (m + 1) → ℝ)
(hw : ∀ i, 0 < w i) :
∀ᶠ H : ℝ in atTop,
(∏ i : Fin (m + 1), ((⌈H / w i⌉₊ + 1 : ℕ) : ℝ)) ≤
(∏ i : Fin (m + 1), (1 / w i + 2)) * (H + 1) ^ (m + 1) := by sorrySource