OAI/Combinatorics/EditApproximation/Geometry/UnskippedRegretBudget.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual guarded band supplies the mass and entropy factors in the node budget.

  1. theorem OAI.EditApproximation.band_dimension_log_of_computed line 12
  2. theorem OAI.EditApproximation.unskipped_expected_regret_budget line 21