OAI/MathematicalPhysics/Boltzmann/Branching/ExponentialPairIntegrability.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Integrable exponential collision pairs from the common squared moment envelope

  1. def OAI.BoltzmannNonuniqueness.CollisionCompactness.exponentialPair line 16
  2. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.exponentialPair_measurable line 19
  3. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.exponentialPair_nonneg line 25
  4. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.exponentialPair_integrable line 30