OAI/MathematicalPhysics/Boltzmann/Collision/VelocityPolynomialBounds.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Hard-sphere pair rates controlled by the half-Gaussian moment

  1. theorem OAI.BoltzmannNonuniqueness.VelocityMoment.norm_le_weight line 16
  2. theorem OAI.BoltzmannNonuniqueness.VelocityMoment.pair_weight_le line 21
  3. def OAI.BoltzmannNonuniqueness.VelocityMoment.pairMoment line 29
  4. theorem OAI.BoltzmannNonuniqueness.VelocityMoment.moment_tensor line 32
  5. theorem OAI.BoltzmannNonuniqueness.VelocityMoment.pairMoment_le line 39
  6. theorem OAI.BoltzmannNonuniqueness.VelocityMoment.pairMoment_le_square line 59
  7. def OAI.BoltzmannNonuniqueness.VelocityMoment.pairTailSet line 85
  8. def OAI.BoltzmannNonuniqueness.VelocityMoment.pairTail line 86
  9. theorem OAI.BoltzmannNonuniqueness.VelocityMoment.pairTailSet_measurable line 89
  10. theorem OAI.BoltzmannNonuniqueness.VelocityMoment.norm_le_quarter line 93
  11. theorem OAI.BoltzmannNonuniqueness.VelocityMoment.pair_tail_weight_le line 97
  12. theorem OAI.BoltzmannNonuniqueness.VelocityMoment.pairTail_le line 120
  13. theorem OAI.BoltzmannNonuniqueness.VelocityMoment.pairTail_le_square line 146
  14. theorem OAI.BoltzmannNonuniqueness.VelocityMoment.norm_sq_le_weight line 171
  15. theorem OAI.BoltzmannNonuniqueness.VelocityMoment.norm_cube_le_weight line 176
  16. theorem OAI.BoltzmannNonuniqueness.VelocityMoment.norm_sq_kernel_le_weight line 185