OAI/MathematicalPhysics/Boltzmann/Branching/ClippedCharacteristicGain.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Actual gain limits with bounded spatial mass and a fixed elastic window

  1. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.clippedFiniteGain line 19
  2. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.clippedPhysicalGain line 22
  3. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.clippedFiniteGain_measurable line 25
  4. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.clippedPhysicalGain_measurable line 30
  5. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.clipped_gain_limit line 35
  6. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.clip_mul_div_bounds line 94
  7. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.regularizedPostRate_fiber_full_integrable line 103
  8. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.clippedFiniteGain_bounds line 124
  9. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.clippedPostRate line 168
  10. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.clippedPostRate_measurable line 172
  11. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.clippedPostRate_bounds line 178
  12. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.clippedPostRate_eventually_full line 194
  13. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.clippedPhysicalGain_tendsto line 206
  14. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.clippedPhysicalGain_nonneg line 223
  15. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.characteristicClippedFiniteGain line 243
  16. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.characteristicClippedPhysicalGain line 246
  17. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.characteristicClippedFiniteGain_measurable line 249
  18. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.characteristicClippedPhysicalGain_measurable line 255
  19. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.characteristic_clipped_gain_limit line 261