PhysicalProgramNodeRegret.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Actual local and global expected regret of the complete finite selection program.

def OAI.EditApproximation.physicalProgramNodeCoefficient line 12
theorem OAI.EditApproximation.physicalProgram_conditional_node_regret line 85
Source documentation
The actual program satisfies the fixed-child conditional node bound; both candidate-list premises and both deeper-agreement premises are proved.
```
theorem physicalProgram_conditional_node_regret (draw : Draw) (S : ℕ) :
    let c : ℝ := stateEditCost (physicalSource source node.1) target q
…
```
Mentions: OAI.EditApproximation.stateEditCost, OAI.EditApproximation.physicalSource
theorem OAI.EditApproximation.physicalProgram_global_node_regret line 126
Source documentation
The actual complete program has the node budget in its original finite product law. The two selected arrays are independently refreshed, and all complete child histories stay fixed.
```
theorem physicalProgram_global_node_regret (S : ℕ) :
    let c : ℝ := stateEditCost (physicalSource source node.1) target q
…
```
Mentions: OAI.EditApproximation.stateEditCost, OAI.EditApproximation.physicalSource