Degree below m, internally

The public statements bound degrees with natDegree f < n, a comparison of natural numbers. That formulation cannot express P_{3,0} = {0}, because the zero polynomial has natural degree 0; and the recursion of the construction starts exactly there. So internally a polynomial has degree below m when degree f < m in WithBot ℕ, where m = 0 says f = 0 and no separate base case is needed. The two agree for m ≥ 1, which is where the public statements live.

This file is the toolkit: the coefficient characterisation, the passage to natDegree, closure under the operations the lift performs, and the two multiplication bounds for P and Q.

def NaslundCounterexample.Below (m : ℕ) (f : Polynomial (ZMod 3)) : Prop

f has degree below m: membership in P_{3,m}, the polynomials of degree less than m. For m = 0 this says f = 0, since degree 0 = ⊥.

Equations

• NaslundCounterexample.Below m f = (f.degree < ↑m)

def NaslundCounterexample.AllBelow (m : ℕ) (B : Finset (Polynomial (ZMod 3))) : Prop

Every element of B has degree below m, that is, B ⊆ P_{3,m}.

Equations

• NaslundCounterexample.AllBelow m B = ∀ f ∈ B, NaslundCounterexample.Below m f

theorem NaslundCounterexample.below_iff_coeff (m : ℕ) (f : Polynomial (ZMod 3)) : Below m f ↔ ∀ (i : ℕ), m ≤ i → f.coeff i = 0

Degree below m read off the coefficients: all coefficients from T^m on vanish.

theorem NaslundCounterexample.Below.coeff_eq_zero {m : ℕ} {f : Polynomial (ZMod 3)} (h : Below m f) {i : ℕ} (hi : m ≤ i) : f.coeff i = 0

The coefficients of a polynomial of degree below m vanish from T^m on.

theorem NaslundCounterexample.below_zero_iff (f : Polynomial (ZMod 3)) : Below 0 f ↔ f = 0

P_{3,0} = {0}: degree below 0 is exactly being the zero polynomial.

theorem NaslundCounterexample.below_iff_natDegree_lt (m : ℕ) (f : Polynomial (ZMod 3)) (hm : 1 ≤ m) : Below m f ↔ f.natDegree < m

For m ≥ 1, degree below m is the public bound natDegree f < m.

theorem NaslundCounterexample.allBelow_iff_degreeBelow (m : ℕ) (B : Finset (Polynomial (ZMod 3))) (hm : 1 ≤ m) : AllBelow m B ↔ DegreeBelow m B

For m ≥ 1, the internal and the public degree bounds on a finite set agree.

theorem NaslundCounterexample.Below.mono {m m' : ℕ} (h : m ≤ m') {f : Polynomial (ZMod 3)} (hf : Below m f) : Below m' f

A degree bound may be weakened.

theorem NaslundCounterexample.Below.natDegree_le {m : ℕ} {f : Polynomial (ZMod 3)} (h : Below (m + 1) f) : f.natDegree ≤ m

Degree below m + 1 is natural degree at most m.

theorem NaslundCounterexample.below_zero (m : ℕ) : Below m 0

The zero polynomial has degree below every m, including m = 0.

theorem NaslundCounterexample.below_of_degree_le {m : ℕ} {f : Polynomial (ZMod 3)} (h : f.degree ≤ ↑m) : Below (m + 1) f

Degree at most m is degree below m + 1.

theorem NaslundCounterexample.Below.add {m : ℕ} {f g : Polynomial (ZMod 3)} (hf : Below m f) (hg : Below m g) : Below m (f + g)

A sum of polynomials of degree below m has degree below m.

theorem NaslundCounterexample.Below.neg {m : ℕ} {f : Polynomial (ZMod 3)} (hf : Below m f) : Below m (-f)

Negation preserves the degree bound.

theorem NaslundCounterexample.Below.sub {m : ℕ} {f g : Polynomial (ZMod 3)} (hf : Below m f) (hg : Below m g) : Below m (f - g)

A difference of polynomials of degree below m has degree below m.

theorem NaslundCounterexample.below_C_mul_X_pow (a : ZMod 3) (i m : ℕ) (h : i < m) : Below m (Polynomial.C a * Polynomial.X ^ i)

A single term a T^i with i < m has degree below m.

theorem NaslundCounterexample.Below.P_mul {m : ℕ} {f : Polynomial (ZMod 3)} (h : Below m f) : Below (m + 3) (P * f)

Multiplying by P raises the degree bound by 3.

theorem NaslundCounterexample.Below.Q_mul {m : ℕ} {f : Polynomial (ZMod 3)} (h : Below m f) : Below (m + 6) (Q * f)

Multiplying by Q raises the degree bound by 6.