OAI/Algebra/DepthFive/IndexedCircuitValue.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem335.IndexedDepth5Circuit.bottomValue line 14

   Source documentation

   Value of a bottom gate before relabelling the gate types.

   def bottomValue (c : IndexedDepth5Circuit K n L B P M U) (i : B) :
       MvPolynomial (Fin n × Fin n × Fin n) K :=
   …

   Mentions: OAI.Problem335.IndexedDepth5Circuit

2. def OAI.Problem335.IndexedDepth5Circuit.lowerValue line 20

   Source documentation

   Value of a lower product gate before relabelling the gate types.

   def lowerValue (c : IndexedDepth5Circuit K n L B P M U) (i : P) :
       MvPolynomial (Fin n × Fin n × Fin n) K :=
   …

   Mentions: OAI.Problem335.IndexedDepth5Circuit

3. def OAI.Problem335.IndexedDepth5Circuit.middleValue line 25

   Source documentation

   Value of a middle sum gate before relabelling the gate types.

   def middleValue (c : IndexedDepth5Circuit K n L B P M U) (i : M) :
       MvPolynomial (Fin n × Fin n × Fin n) K :=
   …

   Mentions: OAI.Problem335.IndexedDepth5Circuit

4. def OAI.Problem335.IndexedDepth5Circuit.upperValue line 31

   Source documentation

   Value of an upper product gate before relabelling the gate types.

   def upperValue (c : IndexedDepth5Circuit K n L B P M U) (i : U) :
       MvPolynomial (Fin n × Fin n × Fin n) K :=
   …

   Mentions: OAI.Problem335.IndexedDepth5Circuit

5. def OAI.Problem335.IndexedDepth5Circuit.circuitValue line 36

   Source documentation

   Polynomial computed by a circuit indexed by arbitrary finite types.

   def circuitValue (c : IndexedDepth5Circuit K n L B P M U) :
       MvPolynomial (Fin n × Fin n × Fin n) K :=
   …

   Mentions: OAI.Problem335.IndexedDepth5Circuit

6. theorem OAI.Problem335.IndexedDepth5Circuit.bottomValue_toDepth5Circuit line 43
7. theorem OAI.Problem335.IndexedDepth5Circuit.lowerValue_toDepth5Circuit line 50
8. theorem OAI.Problem335.IndexedDepth5Circuit.middleValue_toDepth5Circuit line 57
9. theorem OAI.Problem335.IndexedDepth5Circuit.upperValue_toDepth5Circuit line 65
10. theorem OAI.Problem335.IndexedDepth5Circuit.circuitValue_toDepth5Circuit line 73