OAI/Combinatorics/ParityLifts/ParameterPolynomial.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.ParityWL.Complexity.ParamPolyProgram line 9

   Source documentation

   A single finite program, polynomial on each fixed parameter fibre. The parameter is genuine input data, not an infinite family of finite controls.

   structure ParamPolyProgram (ρ α β : Type) [TreeCodec ρ] [TreeCodec α] [TreeCodec β]
       (f : ρ → α → β) where
   …

   Mentions: OAI.ParityWL.Complexity.TreeCodec

2. def OAI.ParityWL.Complexity.ParamPolyProgram.ofPoly line 16
3. def OAI.ParityWL.Complexity.ParamPolyProgram.pair line 23
4. def OAI.ParityWL.Complexity.ParamPolyProgram.comp line 34
5. lemma OAI.ParityWL.Complexity.TreeProgram.fixed_fold_polynomial line 70