OAI/MathematicalPhysics/Boltzmann/Branching/IncomingLossRate.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Continuous incoming-velocity tests for the symmetric gain and loss

These use the original normal-sphere parametrization, so no new change of variables is needed to handle the diagonal where the two velocities coincide.

  1. def OAI.BoltzmannNonuniqueness.CollisionCompactness.incomingGainTest line 21
  2. def OAI.BoltzmannNonuniqueness.CollisionCompactness.incomingLossTest line 25
  3. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.incomingGainTest_continuous line 28
  4. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.incomingLossTest_continuous line 40
  5. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.incomingGainTest_abs_le line 45
  6. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.incomingLossTest_abs_le line 67
  7. def OAI.BoltzmannNonuniqueness.CollisionCompactness.incomingRate line 93
  8. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.incomingRate_nonneg line 96
  9. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.incomingRate_measurable line 102
  10. def OAI.BoltzmannNonuniqueness.CollisionCompactness.incomingCollisionMeasure line 106
  11. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.incomingCollisionMeasure_mass line 111
  12. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.incomingCollisionMeasure_finite line 127
  13. def OAI.BoltzmannNonuniqueness.CollisionCompactness.incomingLeft line 134
  14. def OAI.BoltzmannNonuniqueness.CollisionCompactness.incomingRight line 137
  15. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.incomingLeft_measurable line 140
  16. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.incomingRight_measurable line 144
  17. def OAI.BoltzmannNonuniqueness.CollisionCompactness.incomingGainMeasure line 148
  18. def OAI.BoltzmannNonuniqueness.CollisionCompactness.incomingLossMeasure line 152
  19. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.incomingGainMeasure_mass line 155
  20. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.incomingLossMeasure_mass line 164
  21. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.incomingGainMeasure_finite line 168
  22. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.incomingLossMeasure_finite line 173
  23. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.incomingCollisionMeasure_integral line 197
  24. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.incomingGainMeasure_integral line 213
  25. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.incomingLossMeasure_integral line 229
  26. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.incomingCollisionMeasure_integral_prod line 254
  27. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.incomingCollision_weight_integrable line 297
  28. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.incomingTests_linear_growth line 333
  29. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.incomingGainMeasure_separated line 364
  30. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.incomingLossMeasure_separated line 410
  31. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.incomingRate_integrable_of_gaussian line 451
  32. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.incomingLossMeasure_rate_integral line 487