OAI/GroupTheory/PolycyclicRecognition/Analysis/RemezInput.lean

Scalar polynomial sublevel estimates

M. I. Ganzburg, A multivariate Remez-type inequality with φ-concave weights, Colloquium Mathematicum 147 (2017), 221–240, Theorem 1.2(a), p. 222, DOI 10.4064/cm6884-7-2016.

The sharp estimate gives a coarse cube specialization. Its Chebyshev factor is bounded by (4 n |V| / |S|)^D, using 1 - (1 - t)^(1/n) ≥ t/n and T_D(x) ≤ (2*x)^D for x ≥ 1. For the cube V = [-R,R]^n, its volume is at most 2^n (1+R)^n. A fixed constant absorbs these factors. Coordinate slicing also proves the weaker exponent n * D, which suffices for the image-volume estimates.