OAI/Combinatorics/EditApproximation/Binary/BinaryDyadicSampledGroups.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The generated binary scale list is reindexed into the finite draw domain. Only proof transport is used: the accepted draw count is the same natural computed by groupSampleCountWithWork.

  1. theorem OAI.EditApproximation.BinaryFraction.indexedGroupScales_value line 16
  2. theorem OAI.EditApproximation.BinaryFraction.unskippedEstimate_scale_transport line 25
  3. def OAI.EditApproximation.BinaryFraction.dyadicSampledGroupActionWithWork line 51
  4. theorem OAI.EditApproximation.BinaryFraction.dyadicSampledGroupActionWithWork_value line 57