OAI/Combinatorics/EditApproximation/Refinement/PhysicalSubtreeMass.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Actual original-table warmup masses below an arbitrary physical node.

  1. def OAI.EditApproximation.subtreeComparisonMass line 24

    Source documentation

    The comparison mass is the actual averaged warmup at active states and true cost at carried stopped states.

    noncomputable def subtreeComparisonMass (d : ℕ) (path : TreeLayer M d) : ℝ :=
…

    Mentions: OAI.EditApproximation.TreeLayer

  2. def OAI.EditApproximation.subtreeComparisonEnergy line 28
  3. theorem OAI.EditApproximation.subtreeComparisonMass_bounds line 34
  4. theorem OAI.EditApproximation.subtreeComparisonEnergy_bounds line 50
  5. theorem OAI.EditApproximation.subtreeComparisonMass_root line 61
  6. theorem OAI.EditApproximation.subtreeComparisonMass_terminal line 69
  7. theorem OAI.EditApproximation.subtreeComparisonEnergy_telescope line 76
  8. theorem OAI.EditApproximation.subtreeComparisonMass_step_stopped line 106
  9. theorem OAI.EditApproximation.subtreeComparisonEnergy_step_stopped line 127
  10. theorem OAI.EditApproximation.subtreeComparison_step_none line 151
  11. theorem OAI.EditApproximation.subtreeComparisonMass_step_active line 163
  12. theorem OAI.EditApproximation.subtreeComparisonEnergy_step_active line 185