OAI/MathematicalPhysics/Boltzmann/Branching/OuterTightness.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Fixed outer-annulus majorants give tightness in all velocity variables

  1. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.outer_unifTight_of_bound line 18
  2. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.outer_density_unifTight line 38
  3. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.outer_pairs_unifTight line 57
  4. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.outer_gainLoss_unifTight line 73