OAI/Combinatorics/ContingencyTables/Transport/MeasuredMap.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ContingencyTables.MeasuredMap.mapStep_cost line 14

   Source documentation

   The map accumulator adds linear copying overhead to one call of the underlying computation. Its cost may use an external finite-box measure.

   lemma mapStep_cost {f : A×B → C} (F : Realizer f) (a : A) (b : B) (cs : List C) :
       (mapStepRealizer F).cost (b,(a,cs)) ≤
         F.cost (a,b)+500*(weight a+weight b+weight cs+weight (f (a,b))+1) := by
   …

2. def OAI.ContingencyTables.MeasuredMap.listMeasure line 21
3. def OAI.ContingencyTables.MeasuredMap.foldMeasure line 24
4. lemma OAI.ContingencyTables.MeasuredMap.measure_entry line 27
5. lemma OAI.ContingencyTables.MeasuredMap.work_mapWith line 35

   Source documentation

   Mapping a finite list costs a polynomial in its encoded size and in the sum of the work measures of its individual cached computations.

   lemma work_mapWith {f : A×B → C} (F : Realizer f) (μ : A×B → ℕ)
       (hF : WorkBound F μ) : WorkBound (mapWith F) (listMeasure μ) := by
   …

   Mentions: OAI.ContingencyTables.MeasuredMap.listMeasure