OAI/Combinatorics/EditApproximation/Geometry/LocalRandomSourceCost.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Source charges survive the two adaptive data-gathering stages unchanged. All table reads have weight zero here; their dependency cost is accounted for by the projected table program. No accuracy event is used.

  1. theorem OAI.EditApproximation.localRandomBandDataQuery_source_cost_le line 33
  2. theorem OAI.EditApproximation.localRandomDataQuery_source_cost_le line 47