OAI/Combinatorics/ParityLifts/LeafBounds.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ParityWL.Complexity.PolyProgram.wordsOutput_degree_form line 7
2. lemma OAI.ParityWL.Complexity.PolyProgram.wordsOutput_degree line 12
3. lemma OAI.ParityWL.Complexity.TreeProgram.leafOutput_time line 17
4. lemma OAI.ParityWL.Complexity.TreeProgram.insertWords_time line 24
5. lemma OAI.ParityWL.Complexity.tableInput_size line 29
6. lemma OAI.ParityWL.Complexity.leaf_numeric_bound line 36
7. theorem OAI.ParityWL.Complexity.leafOutput_bound line 90

   Source documentation

   All exponential work in a leaf has an absolute exponent.

   theorem leafOutput_bound : ∃ E : ℕ, 0<E ∧ ∀ (t : ℕ) [NeZero t] (ht : 0<t), ∃ C d : ℕ,
       0<C ∧ ∀ F : BitFormula, (TreeProgram.leafOutput t ht).time F ≤
         C*((treeEncode F).size+1)^d * 2^(E*leafWords t F) := by
   …

   Mentions: OAI.ParityWL.Complexity.BitFormula, OAI.ParityWL.Complexity.TreeProgram.leafOutput, OAI.ParityWL.Complexity.treeEncode, OAI.ParityWL.Complexity.leafWords