Documentation

LeanPool.CCDN.AuxiliaryPolynomial.HypersurfaceKernelRatio

The homogeneous kernel-to-rank ratio differs from its leading term by at most 1/M. Exact binomial identities avoid a formal asymptotic expansion.

theorem CCDN.hypersurface_kernel_ratio_bounds {r d M s : ℕ} (hd : 0 < d) (hdM : d ≤ M) (hr : s + (r + 1 + (M - d)).choose (M - d) = (r + 1 + M).choose M) :
1 / (↑d * (↑r + 1)) - 1 / ↑M ≤ ↑((r + 1 + (M - d)).choose (M - d)) / (↑M * ↑s) ∧ ↑((r + 1 + (M - d)).choose (M - d)) / (↑M * ↑s) ≤ 1 / (↑d * (↑r + 1)) + 1 / ↑M

Sharp leading term for the fraction of polynomial coefficients in the homogeneous kernel, normalized by degree and rank.