PhysicalProgramComparisonRegret.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The actual selection program supplies the good-node premise of the comparison-tree expected-regret telescope.

theorem OAI.EditApproximation.computed_program_grid_lower line 16

theorem OAI.EditApproximation.physicalProgram_comparison_node_regret line 61

Source documentation

Non-bad, low-prediction comparison slots use their literal accepted representative and whole-cell random coordinates in the global program.

theorem physicalProgram_comparison_node_regret (S : ℕ) (d : Fin J) (path : TreeLayer M d.val)
    (hnotbad : ¬ (comparisonActiveScale source target (frontier d.val path) <
      heightQuarterRoot N * (charges d path).1 ∨
      comparisonActiveScale source target (frontier d.val path) < heightQuarterRoot N * (charges d path).2))
    (hvelocity : |prediction d path| ≤ 1 - tau) :
    (∫ draw : Draw, (∑ t ∈ range S, physicalComparisonTreeRegret source target hM U N P F A hP T delta
      (choices draw) rootQ t d path) ∂globalLaw) ≤
      physicalProgramNodeCoefficient N F η κ delta S H * comparisonActiveCost source target (frontier d.val path) := by
…

Mentions: OAI.EditApproximation.TreeLayer, OAI.EditApproximation.comparisonActiveScale, OAI.EditApproximation.heightQuarterRoot, OAI.EditApproximation.physicalComparisonTreeRegret, OAI.EditApproximation.physicalProgramNodeCoefficient, OAI.EditApproximation.comparisonActiveCost