OAI/MathematicalPhysics/Boltzmann/Branching/BackwardCellBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Every bounded endpoint path lies in the dilated fundamental box eventually

  1. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.backward_path_in_cell line 14