OAI/Combinatorics/EditApproximation/Refinement/PhysicalWarmup.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Warmup on physical node labels

The Bellman operator requests only physical children. Distinct child labels are retained even at repeated cuts. Nodes at the last physical level, and source intervals of width at most one, retain their initial value.

  1. theorem OAI.EditApproximation.physicalSourceInterval_child line 27
  2. def OAI.EditApproximation.physicalLower line 31
  3. def OAI.EditApproximation.physicalBellman line 36
  4. theorem OAI.EditApproximation.physicalBellman_monotone line 48
  5. theorem OAI.EditApproximation.physicalBellman_le_initial line 63
  6. theorem OAI.EditApproximation.physicalBellman_lower line 77
  7. def OAI.EditApproximation.physicalWarmup line 97
  8. def OAI.EditApproximation.physicalWarmupAverage line 103
  9. theorem OAI.EditApproximation.physicalBellman_le_action line 109
  10. theorem OAI.EditApproximation.physicalWarmup_average_sandwich line 138
  11. theorem OAI.EditApproximation.physicalWarmup_average_action_bound line 149
  12. theorem OAI.EditApproximation.physicalWarmup_nonincreasing line 170
  13. theorem OAI.EditApproximation.physicalWarmup_lower line 178