Lemma 16 — CLP Polynomial Tensor Product Ratio Strict Decay
Provedclp_tensor_product_sublinear_decayanalysiscombinatoricserdos-problemsnumber-theory
For polynomial evaluation operators on product spaces with C < N, the power-law ratio (C/N)^n strictly decays below 1.
Formal statement
import Mathlib
theorem clp_tensor_product_sublinear_decay (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