OAI/Combinatorics/EditApproximation/Geometry/WarmupReadWork.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Literal seed, initial-cone and warmup query counts. No accuracy event is needed: even rejected local centers are included in these bounds.

  1. theorem OAI.EditApproximation.rawInitialConeCenters_length line 11
  2. theorem OAI.EditApproximation.physicalInitialQuery_cost_le line 34
  3. theorem OAI.EditApproximation.localWarmupStepQuery_cost_le line 63
  4. theorem OAI.EditApproximation.chargedSeedQuery_cost_le line 118
  5. theorem OAI.EditApproximation.chargedWarmupQuery_cost_le line 128