inductive Formula (α : Type u) (n : ℕ) : Type u

• Var {α : Type u} {n : ℕ} (x : Fin n) : Formula α n
• Add {α : Type u} {n : ℕ} (g h : Formula α n) : Formula α n
• Mult {α : Type u} {n : ℕ} (g h : Formula α n) : Formula α n
• Neg {α : Type u} {n : ℕ} (g : Formula α n) : Formula α n
• Const {α : Type u} {n : ℕ} (c : α) : Formula α n

def «termC[_]» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def «termV[_]» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

instance zero {α : Type u_1} {n : ℕ} [Ring α] : Zero (Formula α n)

Equations

• zero = { zero := C[0] }

instance one {α : Type u_1} {n : ℕ} [Ring α] : One (Formula α n)

Equations

• one = { one := C[1] }

instance add {α : Type u_1} {n : ℕ} [Ring α] : Add (Formula α n)

Equations

• add = { add := Formula.Add }

instance neg {α : Type u_1} {n : ℕ} [Ring α] : Neg (Formula α n)

Equations

• neg = { neg := Formula.Neg }

instance sub {α : Type u_1} {n : ℕ} [Ring α] : Sub (Formula α n)

Equations

• sub = { sub := fun (a b : Formula α n) => a + -b }

instance mul' {α : Type u_1} {n : ℕ} [Ring α] : Mul (Formula α n)

Equations

• mul' = { mul := Formula.Mult }

def size {α : Type u_1} {n : ℕ} (f : Formula α n) : ℕ

Equations

• size (Formula.Var x) = 0
• size (g.Add h) = size g + size h + 1
• size (g.Mult h) = size g + size h + 1
• size g.Neg = size g + 1
• size C[c] = 0

def depth {α : Type u_1} {n : ℕ} (f : Formula α n) : ℕ

Equations

• depth (Formula.Var x) = 0
• depth (g.Add h) = depth g ⊔ depth h + 1
• depth (g.Mult h) = depth g ⊔ depth h + 1
• depth g.Neg = depth g + 1
• depth C[c] = 0

noncomputable def evalToPolynomial {α : Type u_1} {n : ℕ} [CommRing α] (f : Formula α n) : MvPolynomial (Fin n) α

Equations

• evalToPolynomial (Formula.Var x) = MvPolynomial.X x ^ 1
• evalToPolynomial (g.Add h) = evalToPolynomial g + evalToPolynomial h
• evalToPolynomial (g.Mult h) = evalToPolynomial g * evalToPolynomial h
• evalToPolynomial g.Neg = -evalToPolynomial g
• evalToPolynomial C[c] = MvPolynomial.C c

theorem size_zero_const_or_var {α : Type u_1} {n : ℕ} (f : Formula α n) : size f = 0 → (∃ (x : Fin n), f = Formula.Var x) ∨ ∃ (c : α), f = C[c]

theorem size_highest_degree {α : Type u_1} {n : ℕ} [CommRing α] [Nontrivial α] (f : Formula α n) : size f ≥ (evalToPolynomial f).totalDegree - 1

def coerce_up {α : Type u_1} {n : ℕ} (f : Formula α n) : Formula α (n + 1)

coerce_up f coerces a formula f in n variables to a formula in n + 1 variables.

Equations

• coerce_up (Formula.Var x) = Formula.Var ↑↑x
• coerce_up (g.Add h) = (coerce_up g).Add (coerce_up h)
• coerce_up (g.Mult h) = (coerce_up g).Mult (coerce_up h)
• coerce_up g.Neg = (coerce_up g).Neg
• coerce_up C[c] = C[c]

instance instCoeFormulaHAddNatOfNat {α : Type u_1} {n : ℕ} : Coe (Formula α n) (Formula α (n + 1))

This is the Coe typeclass instance for the above coercion. T

Equations

• instCoeFormulaHAddNatOfNat = { coe := fun (f : Formula α n) => coerce_up f }

noncomputable def incrVar {α : Type u_1} {n : ℕ} [CommSemiring α] (p : MvPolynomial (Fin n) α) : MvPolynomial (Fin (n + 1)) α

incrVar p coerces an n variable MvPolynomial to an n + 1 variable MvPolynomial

Equations

• incrVar p = (MvPolynomial.rename Fin.castSucc) p

@[simp]

theorem incrVar_composes_add {α : Type u_1} {n : ℕ} [CommSemiring α] (f g : MvPolynomial (Fin n) α) : incrVar f + incrVar g = incrVar (f + g)

The three lemmas below show that the incrVar function respects ring operations on the polynomial.

@[simp]

theorem incrVar_composes_mult {α : Type u_1} {n : ℕ} [CommSemiring α] (f g : MvPolynomial (Fin n) α) : incrVar f * incrVar g = incrVar (f * g)

@[simp]

theorem incrVar_composes_neg {α : Type u_1} {n : ℕ} [CommRing α] (f : MvPolynomial (Fin n) α) : -incrVar f = incrVar (-f)

noncomputable instance instCoeMvPolynomialFinHAddNatOfNat_algebraicComplexity {α : Type u_1} {n : ℕ} [CommSemiring α] : Coe (MvPolynomial (Fin n) α) (MvPolynomial (Fin (n + 1)) α)

Equations

• instCoeMvPolynomialFinHAddNatOfNat_algebraicComplexity = { coe := fun (p : MvPolynomial (Fin n) α) => incrVar p }

theorem coerce_up_preserves_incrVar_eval {α : Type u_1} {n : ℕ} [CommRing α] (f : Formula α n) (p : MvPolynomial (Fin n) α) : evalToPolynomial f = p → evalToPolynomial (coerce_up f) = incrVar p

def L (n : ℕ) (α : Type u) [CommRing α] (p : MvPolynomial (Fin n) α) (k : ℕ) : Prop

Equations

• L n α p k = ∃ (f : Formula α n), evalToPolynomial f = p ∧ (∀ (g : Formula α n), evalToPolynomial g = p → k ≤ size g) ∧ size f = k

theorem complexity_monomial {α : Type u_1} [iCRα : CommRing α] [ntα : Nontrivial α] (n d : ℕ) (hn_pos : n > 0) (hd_pos : d > 0) : ∃ (k : ℕ), L (n + 1) α (MvPolynomial.X ⟨0, ⋯⟩ ^ d) k ∧ k = d - 1