OAI/MathematicalPhysics/Boltzmann/Collision/AngularGainTranslationTests.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Compact incoming-velocity bounds for bounded angular tests

  1. instance OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.incomingBallFinite line 15
  2. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.angularAdjoint_abs_le line 20
  3. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.angularAdjoint_bounded_on line 33
  4. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.angularAdjoint_integrableOn line 44
  5. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.angularAdjoint_square_integrableOn line 53
  6. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.angularAdjoint_translation_square line 77
  7. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.angularAdjoint_translation_L1 line 110
  8. def OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.angularFamily line 141
  9. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.angularFamily_measurable line 144
  10. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.angularFamily_integrable line 160
  11. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.angularFamily_translation_L1 line 173
  12. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.bounded_gain_translation_tests line 230