OAI/Combinatorics/EditApproximation/Geometry/GroupSamplingWork.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The shared group samples cancel the reciprocal envelope factor in the number of possible rounded child inputs, including exact evaluation.

  1. theorem OAI.EditApproximation.groupSampleCount_shared_work line 10
  2. theorem OAI.EditApproximation.groupDyadicScale_shared_work line 45