OAI/Combinatorics/EditApproximation/Refinement/PhysicalRefinement.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The complete physical refinement recurrence. Current-index recursive requests go only to physical children. The selection interface records literal wide list membership, and carries no approximation or probability assumption.

  1. structure OAI.EditApproximation.PhysicalSelections line 21
  2. def OAI.EditApproximation.physicalRefinement line 31
  3. theorem OAI.EditApproximation.physicalRefinement_at_leaf line 56
  4. theorem OAI.EditApproximation.physicalRefinement_at_last_level line 71
  5. theorem OAI.EditApproximation.physicalRefinement_succ line 81