OAI/Combinatorics/EditApproximation/Refinement/PhysicalConditionalNode.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Conditional expected regret in a fixed child environment

Finite Bernstein bounds control the parent product draws. Agreement of deeper selection functions fixes all child histories by locality, and list membership connects the sampled actions to the refinement recurrence.

  1. abbrev OAI.EditApproximation.BandParentSpace line 18
  2. def OAI.EditApproximation.bandParentLaw line 22
  3. theorem OAI.EditApproximation.physical_conditional_node_regret line 27