Degree: 19 declarations
On this page · Permalink · Source line 845
L041 bprod_nil
On this page · Permalink · Source line 847
Source. CircuitObstructions/Degree.lean:19
Block. 02 Axioms. none
CircuitObstructions.bprod_nil {W : Type} (s : CircuitObstructions.State W) : CircuitObstructions.bprod [] s = trueL042 bprod_cons
On this page · Permalink · Source line 856
Source. CircuitObstructions/Degree.lean:20
Block. 02 Axioms. none
CircuitObstructions.bprod_cons {W : Type} (i : W) (is : List W) (s : CircuitObstructions.State W) :
CircuitObstructions.bprod (i :: is) s = (s i && CircuitObstructions.bprod is s)L043 bprod_append
On this page · Permalink · Source line 866
Source. CircuitObstructions/Degree.lean:23
Block. 02 Axioms. propext
CircuitObstructions.bprod_append {W : Type} (l k : List W) (s : CircuitObstructions.State W) :
CircuitObstructions.bprod (l ++ k) s = (CircuitObstructions.bprod l s && CircuitObstructions.bprod k s)L044 xor_and_right
On this page · Permalink · Source line 876
Source. CircuitObstructions/Degree.lean:29
Block. 02 Axioms. none
CircuitObstructions.xor_and_right (a b c : Bool) : ((a ^^ b) && c) = (a && c ^^ b && c)L045 and_xor_right
On this page · Permalink · Source line 885
Source. CircuitObstructions/Degree.lean:33
Block. 02 Axioms. none
CircuitObstructions.and_xor_right (a b c : Bool) : (a && (b ^^ c)) = (a && b ^^ a && c)L046 not_as_xor_one
On this page · Permalink · Source line 894
Source. CircuitObstructions/Degree.lean:37
Block. 02 Axioms. none
CircuitObstructions.not_as_xor_one (a : Bool) : (!a) = (a ^^ true)L047 mono
On this page · Permalink · Source line 903
Source. CircuitObstructions/Degree.lean:47
Block. 02 Axioms. none
CircuitObstructions.DegreeLE.mono {n d e : Nat} {f : CircuitObstructions.BFun n} (h : CircuitObstructions.DegreeLE d f)
(hde : d ≤ e) : CircuitObstructions.DegreeLE e fL048 one
On this page · Permalink · Source line 913
Source. CircuitObstructions/Degree.lean:54
Block. 02 Axioms. none
CircuitObstructions.DegreeLE.one (n d : Nat) : CircuitObstructions.DegreeLE d fun x => trueL049 constant
On this page · Permalink · Source line 922
Source. CircuitObstructions/Degree.lean:57
Block. 02 Axioms. none
CircuitObstructions.DegreeLE.constant (n d : Nat) (b : Bool) : CircuitObstructions.DegreeLE d fun x => bL050 variable
On this page · Permalink · Source line 931
Source. CircuitObstructions/Degree.lean:63
Block. 02 Axioms. propext, Quot.sound
CircuitObstructions.DegreeLE.variable {n : Nat} (i : Fin n) : CircuitObstructions.DegreeLE 1 fun x => x iL051 xor
On this page · Permalink · Source line 940
Source. CircuitObstructions/Degree.lean:67
Block. 02 Axioms. propext
CircuitObstructions.DegreeLE.xor {n d e : Nat} {f g : CircuitObstructions.BFun n}
(hf : CircuitObstructions.DegreeLE d f) (hg : CircuitObstructions.DegreeLE e g) :
CircuitObstructions.DegreeLE (max d e) fun x => f x ^^ g xL052 not
On this page · Permalink · Source line 951
Source. CircuitObstructions/Degree.lean:72
Block. 02 Axioms. Quot.sound
CircuitObstructions.DegreeLE.not {n d : Nat} {f : CircuitObstructions.BFun n} (hf : CircuitObstructions.DegreeLE d f) :
CircuitObstructions.DegreeLE d fun x => !f xL053 monomial_mul
On this page · Permalink · Source line 961
Source. CircuitObstructions/Degree.lean:76
Block. 02 Axioms. propext, Quot.sound
CircuitObstructions.DegreeLE.monomial_mul {n d e : Nat} (l : List (Fin n)) (hl : l.length ≤ d)
{g : CircuitObstructions.BFun n} (hg : CircuitObstructions.DegreeLE e g) :
CircuitObstructions.DegreeLE (d + e) fun x => CircuitObstructions.bprod l x && g xL054 mul
On this page · Permalink · Source line 972
Source. CircuitObstructions/Degree.lean:87
Block. 02 Axioms. propext, Quot.sound
CircuitObstructions.DegreeLE.mul {n d e : Nat} {f g : CircuitObstructions.BFun n}
(hf : CircuitObstructions.DegreeLE d f) (hg : CircuitObstructions.DegreeLE e g) :
CircuitObstructions.DegreeLE (d + e) fun x => f x && g xL055 product
On this page · Permalink · Source line 983
Source. CircuitObstructions/Degree.lean:96
Block. 02 Axioms. propext, Quot.sound
CircuitObstructions.DegreeLE.product {n : Nat} {W : Type} (l : List W)
(s : (Fin n → Bool) → CircuitObstructions.State W) (h : ∀ (i : W), CircuitObstructions.DegreeLE 1 fun x => s x i) :
CircuitObstructions.DegreeLE l.length fun x => CircuitObstructions.bprod l (s x)L056 polyEval_append
On this page · Permalink · Source line 994
Source. CircuitObstructions/Degree.lean:109
Block. 02 Axioms. propext
CircuitObstructions.polyEval_append {n : Nat} (p q : List (List (Fin n))) (x : Fin n → Bool) :
CircuitObstructions.polyEval (p ++ q) x = (CircuitObstructions.polyEval p x ^^ CircuitObstructions.polyEval q x)L057 polynomial_witness
On this page · Permalink · Source line 1004
Source. CircuitObstructions/Degree.lean:115
Block. 02 Axioms. propext, Quot.sound
CircuitObstructions.DegreeLE.polynomial_witness {n d : Nat} {f : CircuitObstructions.BFun n}
(h : CircuitObstructions.DegreeLE d f) :
∃ p, (∀ (l : List (Fin n)), l ∈ p → l.length ≤ d) ∧ CircuitObstructions.polyEval p = fL058 polynomial_degree_certificate
On this page · Permalink · Source line 1015
Source. CircuitObstructions/Degree.lean:134
Block. 02 Axioms. propext
CircuitObstructions.polynomial_degree_certificate {n d : Nat} (p : List (List (Fin n)))
(hp : ∀ (l : List (Fin n)), l ∈ p → l.length ≤ d) : CircuitObstructions.DegreeLE d (CircuitObstructions.polyEval p)L059 degreeLE_iff_polynomial
On this page · Permalink · Source line 1025
Source. CircuitObstructions/Degree.lean:142
Block. 02 Axioms. propext, Quot.sound
CircuitObstructions.degreeLE_iff_polynomial {n d : Nat} (f : CircuitObstructions.BFun n) :
CircuitObstructions.DegreeLE d f ↔
∃ p, (∀ (l : List (Fin n)), l ∈ p → l.length ≤ d) ∧ CircuitObstructions.polyEval p = f