BlockMiddleSemantics.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem335.BlockData.lowerMonomial line 13
Source documentation
The lower-gate monomial belonging to an enumerated block path.
```
def lowerMonomial (K : Type*) [CommSemiring K]
    (blocks : List (List (Fin n))) (p : Lower blocks) :
    MvPolynomial (Fin n × Fin n × Fin n) K :=
…
```
Mentions: OAI.Problem335.BlockData.Lower
theorem OAI.Problem335.BlockData.middleInputs_value line 19
Source documentation
The weighted middle input list computes exactly the corresponding block matrix entry.
```
theorem middleInputs_value (K : Type*) [CommSemiring K]
    (blocks : List (List (Fin n))) (m : Middle blocks) :
    ((middleInputs K blocks m).map (fun e =>
      MvPolynomial.C e.1 * lowerMonomial K blocks e.2)).sum =
      (((blocks.get m.1).map (immLayer K n)).prod) m.2.1 m.2.2 := by
…
```
Mentions: OAI.Problem335.BlockData.Middle, OAI.Problem335.BlockData.middleInputs, OAI.Problem335.BlockData.lowerMonomial, OAI.Problem335.immLayer

theorem OAI.Problem335.BlockData.middleInputs_value_of_lower line 29

Source documentation

Substitute lower-gate semantics into the middle gate.

theorem middleInputs_value_of_lower
    (K : Type*) [CommSemiring K] (blocks : List (List (Fin n)))
    (v : Lower blocks → MvPolynomial (Fin n × Fin n × Fin n) K)
    (hv : ∀ p, v p = lowerMonomial K blocks p) (m : Middle blocks) :
    ((middleInputs K blocks m).map (fun e => MvPolynomial.C e.1 * v e.2)).sum =
      (((blocks.get m.1).map (immLayer K n)).prod) m.2.1 m.2.2 := by
…

Mentions: OAI.Problem335.BlockData.Lower, OAI.Problem335.BlockData.lowerMonomial, OAI.Problem335.BlockData.Middle, OAI.Problem335.BlockData.middleInputs, OAI.Problem335.immLayer