PhysicalProgramSubtreeRegret.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Arbitrary physical subtree slots retain the actual full-table product law.

theorem OAI.EditApproximation.physicalProgram_subtree_node_regret line 53

Source documentation

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

theorem physicalProgram_subtree_node_regret (S : ℕ) (d : Fin K) (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, subtreeComparisonTreeRegret source target hM U N P F A hP T delta
      (choices draw) root K 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.subtreeComparisonTreeRegret, OAI.EditApproximation.physicalProgramNodeCoefficient, OAI.EditApproximation.comparisonActiveCost