Coordinate box bound for strict weighted simplex cardinality
ProvedOAI.PiExponent.DeterminantContradiction.weightedStrictSimplex_box_card_boundnumber-theoryopenai-pi-exponent-017
For any real H and strictly positive weights, the cardinality of the strict weighted simplex is at most the product of the sizes of its coordinate ranges. If H is nonpositive, the strict simplex is empty; for positive H, each coordinate is bounded by the corresponding truncated ceiling.
Preamble
import Definitions.Def_OAI_NumberTheory_PiExponent_Approximation_InterpolationMatrix_Domains import Definitions.Def_OAI_NumberTheory_PiExponent_Polynomials_SimplexCounting_WeightedDomains open scoped BigOperators
Formal statement
theorem OAI.PiExponent.DeterminantContradiction.weightedStrictSimplex_box_card_bound
{m : ℕ} (w : Fin (m + 1) → ℝ)
(hw : ∀ i, 0 < w i) (H : ℝ) :
(Fintype.card {a // a ∈ OAI.PiExponent.strictWeightedSimplex w H} : ℝ) ≤
∏ i : Fin (m + 1), ((⌈H / w i⌉₊ + 1 : ℕ) : ℝ) := by sorrySource