Prove2Me

Lemma 16 — CLP Polynomial Tensor Product Ratio Strict Decay

Proved
clp_tensor_product_sublinear_decay_v3

by Xinyu Xu · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricserdos-problemslinear-algebra

For polynomial evaluation operators on product spaces with C<NC < N, the power-law ratio (C/N)n(C/N)^n strictly decays below 1.

Formal statement
import Mathlib

theorem clp_tensor_product_sublinear_decay_v3 (n : ℕ) (hn : 0 < n) (C N : ℝ)
    (hC_pos : 0 < C) (hC_lt : C < N) (hN_pos : 0 < N) :
    let power_bound : ℝ := C ^ n
    let space_dim : ℝ := N ^ n
    (power_bound / space_dim = (C / N) ^ n) ∧ (C / N < 1) := by sorry

View graph