OAI/MathematicalPhysics/Boltzmann/Branching/VanishingCutoffCollision.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A vanishing local L1 error vanishes against every bounded measurable test

  1. theorem OAI.BoltzmannNonuniqueness.Compactness.integral_tendsto_zero_of_L1 line 20
  2. theorem OAI.BoltzmannNonuniqueness.Compactness.bounded_test_integral_tendsto_zero line 29
  3. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.vanishing_cutoff_collision line 56