Documentation

LeanPool.CCDN.Noether.UniversalPlaneL1

Explicit coefficient-sum bounds for generic plane restrictions. An original monomial of degree d contributes at most 3^d; an Euler matrix entry contributes at most d times this quantity.

theorem CCDN.ambientEulerEntry_monomial_l1_le {σ : Type u_1} (k : ℕ) (m : σ →₀ ℕ) (hm : Finsupp.degree m = k + 2) (row : ℕ × ℕ) (col : EulerColumns k) :
((ambientEulerEntryLinear ℤ σ k row col) ((MvPolynomial.monomial m) 1)).l1Norm ≤ (k + 2) * 3 ^ (k + 2)

For a monomial of degree k + 2, every Euler matrix entry of its universal plane restriction has coefficient ℓ¹-norm at most (k + 2) * 3 ^ (k + 2).