OAI/Combinatorics/EditApproximation/Geometry/LocalRandomDataQuery.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Gather data before selecting a random source coordinate. Online ranges are calculated solely from previously requested band values; group draws and online draws are ordinary scalar reads in the same adaptive query.

  1. theorem OAI.EditApproximation.localRandomBandDataQuery_value line 28
  2. theorem OAI.EditApproximation.localRandomDataQuery_value line 96