OAI/Combinatorics/EditApproximation/Queries/QueryGroupInputs.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A shared estimator requests every child when its exact sample count equals the arity; otherwise it requests the sampled child labels. The Boolean test and each draw-table lookup are included in the counter.

  1. theorem OAI.EditApproximation.BinaryFraction.queryGroupLabelsWithWork_value line 17
  2. theorem OAI.EditApproximation.BinaryFraction.queryGroupInputsWithWork_value line 36