OAI/MathematicalPhysics/Boltzmann/Branching/BoundedPairRate.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform L1 velocity translations of gains from bounded compact incoming densities

  1. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.pairIntegral_localize line 14
  2. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.bounded_pairGain_translation line 30
  3. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.bounded_pairPreRate_integrable line 89
  4. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.bounded_pairGain_translation_no_rate_assumption line 130