OAI/Combinatorics/EditApproximation/Geometry/ComparisonLiftBounds.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Actual stopped-tree warmup masses and their energy telescope bounds.

  1. def OAI.EditApproximation.comparisonStateGap line 12
  2. theorem OAI.EditApproximation.comparisonPhysicalLift_bounds line 17
  3. theorem OAI.EditApproximation.comparisonPhysicalLift_gap line 48
  4. theorem OAI.EditApproximation.gap_energy_bounds line 73
  5. def OAI.EditApproximation.stageComparisonMass line 97

    Source documentation

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

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

    Mentions: OAI.EditApproximation.TreeLayer

  6. def OAI.EditApproximation.stageComparisonEnergy line 101
  7. theorem OAI.EditApproximation.stageComparisonMass_bounds line 107
  8. theorem OAI.EditApproximation.stageComparisonEnergy_bounds line 123
  9. theorem OAI.EditApproximation.stageComparisonMass_root line 134
  10. theorem OAI.EditApproximation.stageComparisonMass_terminal line 142
  11. theorem OAI.EditApproximation.stageComparisonEnergy_telescope line 149