OAI/Combinatorics/EditApproximation/Geometry/LocalRandomTableCost.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Random source reads have zero table charge. Uniform bounds for the remaining local step therefore lift through the actual source collectors, including the adaptive data queries.

  1. theorem OAI.EditApproximation.localRandomSourceStepQuery_table_cost_le line 31
  2. theorem OAI.EditApproximation.localRandomBandDataQuery_table_cost_le line 67
  3. theorem OAI.EditApproximation.localRandomDataQuery_table_cost_le line 118