OAI/Algebra/DepthFive/CircuitFactorForms.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem335.lowerValue_normal_form line 15

   Source documentation

   A lower product computes a scalar times exactly its formal degree many homogeneous linear forms, with repeated inputs retained as repeated factors.

   theorem lowerValue_normal_form (c : Depth5Circuit K n) (i : Fin c.lowerCount) :
       ∃ a : K, ∃ factors : List (MvPolynomial (Fin n × Fin n × Fin n) K),
         factors.length = ((c.lowerInputs i).map c.bottomDegree).sum ∧
         (∀ p ∈ factors, p.IsHomogeneous 1) ∧
         lowerValue c i = MvPolynomial.C a * factors.prod := by
   …

   Mentions: OAI.Problem335.Depth5Circuit, OAI.Problem335.lowerValue

2. theorem OAI.Problem335.middle_input_normal_form line 35

   Source documentation

   A weighted term of a middle sum has a linear-factor form of the middle sum's assigned degree, even for a zero coefficient or zero product.

   theorem middle_input_normal_form (c : Depth5Circuit K n) (i : Fin c.middleCount)
       (entry : K × Fin c.lowerCount) (hentry : entry ∈ c.middleInputs i) :
       ∃ a : K, ∃ factors : List (MvPolynomial (Fin n × Fin n × Fin n) K),
         factors.length = c.middleDegree i ∧
         (∀ p ∈ factors, p.IsHomogeneous 1) ∧
         MvPolynomial.C entry.1 * lowerValue c entry.2 =
           MvPolynomial.C a * factors.prod := by
   …

   Mentions: OAI.Problem335.Depth5Circuit, OAI.Problem335.lowerValue