OAI/Combinatorics/EditApproximation/Binary/IntegerBinaryOutput.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.EditApproximation.integerBinaryOutput line 9

   Source documentation

   Actual binary output on a fixed accepted finite draw.

   def integerBinaryOutput (source target : List ℤ) (N : ℕ)
       (input : ComputedFamilyInput (source.map integerSymbolCode) (target.map integerSymbolCode) N) :=
   …

   Mentions: OAI.EditApproximation.ComputedFamilyInput, OAI.EditApproximation.integerSymbolCode

2. theorem OAI.EditApproximation.integerBinaryOutput_cost line 14
3. theorem OAI.EditApproximation.integerBinaryOutput_execution line 34