Threshold and remainder sets are semilinear (CRN-3)

Helper lemmas for IsSemilinearPred.isSemilinearSet, through Mathlib's semilinear sets: the solutions of a linear equation A + ∑ⱼ pⱼ zⱼ = B + ∑ⱼ p'ⱼ zⱼ over ℕ form a semilinear set (isSemilinearSet_setOf_eq), and semilinear sets are closed under projection (IsSemilinearSet.proj). Write aᵢ = a⁺ᵢ - a⁻ᵢ, c = c⁺ - c⁻ with natural parts; then

• ∑ aᵢ xᵢ < c iff ∃ k, ∑ a⁺ᵢ xᵢ + c⁻ + 1 + k = ∑ a⁻ᵢ xᵢ + c⁺ (one slack variable);
• ∑ aᵢ xᵢ ≡ c (mod m) iff ∃ k₁ k₂, ∑ a⁺ᵢ xᵢ + c⁻ + m k₁ = ∑ a⁻ᵢ xᵢ + c⁺ + m k₂.

def Crn.linForm {κ : Type u_1} [Fintype κ] (p : κ → ℕ) : (κ → ℕ) →+ ℕ

The linear form z ↦ ∑ⱼ pⱼ zⱼ on ℕ-vectors.

Equations

• Crn.linForm p = { toFun := fun (z : κ → ℕ) => ∑ j : κ, p j * z j, map_zero' := ⋯, map_add' := ⋯ }

theorem Crn.isSemilinearSet_linEq {κ : Type u_1} [Fintype κ] (A B : ℕ) (p p' : κ → ℕ) : IsSemilinearSet {z : κ → ℕ | A + ∑ j : κ, p j * z j = B + ∑ j : κ, p' j * z j}

The solutions of a linear equation over ℕ form a semilinear set.

theorem Crn.sum_mul_eq_sub {X : Type u_1} [Fintype X] (a : X → ℤ) (x : X → ℕ) : ∑ i : X, a i * ↑(x i) = ↑(∑ i : X, (a i).toNat * x i) - ↑(∑ i : X, (-a i).toNat * x i)

∑ aᵢ xᵢ = ∑ a⁺ᵢ xᵢ - ∑ a⁻ᵢ xᵢ with the natural parts a⁺ = a.toNat, a⁻ = (-a).toNat.

theorem Crn.isSemilinearSet_threshold {X : Type u_1} [Fintype X] (a : X → ℤ) (c : ℤ) : IsSemilinearSet {x : X → ℕ | threshold a c x = true}

Threshold sets are semilinear.

theorem Crn.isSemilinearSet_remainder {X : Type u_1} [Fintype X] (a : X → ℤ) (c : ℤ) (m : ℕ) : IsSemilinearSet {x : X → ℕ | remainder a c m x = true}

Remainder sets are semilinear.