OAI/Combinatorics/EditApproximation/Queries/QueryLocalSources.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Random words are gathered before the adaptive local selectors run. The online sampling range is computed from the gathered mass words.

  1. def OAI.EditApproximation.queryLocalRandomSources line 27
  2. theorem OAI.EditApproximation.queryLocalRandomSources_refines line 38