OAI/MathematicalPhysics/Boltzmann/Branching/InitialLinearComparison.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Vanishing initial positive-difference error along arbitrary late subsequences

  1. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.initialApproximation_comparison_L1 line 17
  2. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.initialApproximation_linear_comparison_L1 line 57