OAI/Algebra/DepthFive/CoefficientDescent.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem335.restrictLeaf line 13
2. theorem OAI.Problem335.restrictLeaf_degree line 19
3. def OAI.Problem335.restrictWeightedInputs line 24
4. theorem OAI.Problem335.restrictWeightedInputs_eq_nil_iff line 28
5. theorem OAI.Problem335.restrictWeightedInputs_map_coe line 33
6. def OAI.Problem335.restrictCircuit line 39

   Source documentation

   Restrict a circuit to the subfield generated by its occurring coefficients.

   def restrictCircuit (c : Depth5Circuit K n) : Depth5Circuit (circuitCoefficientField c) n where
   …

   Mentions: OAI.Problem335.Depth5Circuit, OAI.Problem335.circuitCoefficientField

7. theorem OAI.Problem335.circuitSize_restrictCircuit line 76
8. theorem OAI.Problem335.map_restrictLeaf_value line 80
9. theorem OAI.Problem335.restrictWeightedInputs_map_eval line 86
10. theorem OAI.Problem335.map_bottomValue_restrictCircuit line 92
11. theorem OAI.Problem335.map_lowerValue_restrictCircuit line 106
12. theorem OAI.Problem335.map_middleValue_restrictCircuit line 116
13. theorem OAI.Problem335.map_upperValue_restrictCircuit line 130
14. theorem OAI.Problem335.map_circuitValue_restrictCircuit line 140