OAI/MathematicalPhysics/Boltzmann/Collision/CollisionSources.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Uniform integrability of the actual cutoff equation's right-hand side

  1. def OAI.BoltzmannNonuniqueness.CollisionCompactness.collisionSource line 20
  2. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.collisionSource_measurable line 23
  3. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.uniformIntegrable_sub line 28
  4. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.collisionSource_uniformIntegrable line 37
  5. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.cutoffFrequency_nonneg line 69
  6. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.collisionSource_le_gain line 75
  7. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.hot_source_le_gain line 82
  8. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.mixedPostRate_const_mul line 109
  9. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.mixedGain_const_mul line 116
  10. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.cutoffGain_const_mul line 124
  11. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.cutoffFrequency_const_mul line 131
  12. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.cutoffFrequency_add line 141
  13. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.mixedPostRate_base_comp line 153
  14. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.mixedGain_base_comp line 158
  15. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.cutoffGain_base_comp line 164
  16. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.cutoffFrequency_base_comp line 170
  17. def OAI.BoltzmannNonuniqueness.CollisionCompactness.collisionMarginal line 191
  18. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.collisionMarginal_integrable line 196
  19. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.collisionMarginal_sub_ae line 201
  20. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.collisionMarginal_eLpNorm_le line 210
  21. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.collisionMarginal_difference_le line 219
  22. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.mixedPostRate_fiber_congr line 246
  23. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.mixedGain_fiber_congr line 256
  24. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.cutoffGain_fiber_congr line 263
  25. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.cutoffFrequency_fiber_congr line 270
  26. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.collisionSource_fiber_congr line 277