OAI/MathematicalPhysics/Boltzmann/Branching/HalfGaussianMoment.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Half-Gaussian velocity moments for the hot weight and cold cores

  1. def OAI.BoltzmannNonuniqueness.VelocityMoment.weight line 15
  2. def OAI.BoltzmannNonuniqueness.VelocityMoment.moment line 16
  3. theorem OAI.BoltzmannNonuniqueness.VelocityMoment.weight_pos line 18
  4. theorem OAI.BoltzmannNonuniqueness.VelocityMoment.weight_one_le line 19
  5. theorem OAI.BoltzmannNonuniqueness.VelocityMoment.weight_le line 20
  6. theorem OAI.BoltzmannNonuniqueness.VelocityMoment.moment_mono line 24
  7. theorem OAI.BoltzmannNonuniqueness.VelocityMoment.moment_mono_ae line 28
  8. theorem OAI.BoltzmannNonuniqueness.VelocityMoment.weight_H_le line 33
  9. theorem OAI.BoltzmannNonuniqueness.VelocityMoment.weight_H_integrable line 44
  10. def OAI.BoltzmannNonuniqueness.VelocityMoment.hotConstant line 52
  11. theorem OAI.BoltzmannNonuniqueness.VelocityMoment.hotConstant_nonneg line 54
  12. theorem OAI.BoltzmannNonuniqueness.VelocityMoment.hot_moment line 57
  13. theorem OAI.BoltzmannNonuniqueness.VelocityMoment.moment_add line 66
  14. theorem OAI.BoltzmannNonuniqueness.VelocityMoment.moment_le_exponential line 78
  15. theorem OAI.BoltzmannNonuniqueness.VelocityMoment.density_integrable line 84