OAI/MathematicalPhysics/Boltzmann/Collision/CollisionDissipation.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

The moving relative-speed cutoff has the full collision limit

  1. def OAI.BoltzmannNonuniqueness.CollisionCompactness.truncatedPreRate line 23
  2. def OAI.BoltzmannNonuniqueness.CollisionCompactness.truncatedPostRate line 27
  3. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.truncatedPreRate_measurable line 31
  4. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.truncatedPostRate_measurable line 35
  5. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.cutoffGain_eq_marginal line 40
  6. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.cutoffLoss_eq_marginal line 51
  7. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.weak_cutoff_gainLoss line 60
  8. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.preRate_congr line 114
  9. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.postRate_congr line 125
  10. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.gainLoss_congr line 130
  11. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.collision_fibers line 144
  12. def OAI.BoltzmannNonuniqueness.CollisionCompactness.particleSwap line 188
  13. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.particleSwap_measurePreserving line 194
  14. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.preRate_particleSwap line 207
  15. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.truncatedPreRate_particleSwap line 217
  16. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.truncatedPreRate_scatter line 225
  17. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.truncatedPostRate_scatter line 235
  18. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.integral_preRate_particleSwap line 240
  19. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.integral_postRate_scatter line 251
  20. theorem OAI.BoltzmannNonuniqueness.scatterLeft_swap line 278
  21. theorem OAI.BoltzmannNonuniqueness.scatterRight_swap line 284
  22. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.scatterTriple_particleSwap line 291
  23. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.postRate_particleSwap line 299
  24. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.truncatedPostRate_particleSwap line 304
  25. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.integral_postRate_particleSwap line 311
  26. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.integral_postRate_scatter_right line 322
  27. def OAI.BoltzmannNonuniqueness.CollisionCompactness.collisionJump line 352
  28. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.cutoff_weak_identity line 356
  29. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.cutoff_collision_invariant line 400
  30. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.preRate_scatter_full line 434
  31. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.postRate_scatter_full line 439
  32. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.integral_preRate_particleSwap_full line 445
  33. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.integral_postRate_scatter_full line 456
  34. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.integral_postRate_particleSwap_full line 467
  35. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.integral_postRate_scatter_right_full line 478
  36. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.full_weak_identity line 489
  37. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.full_collision_invariant line 533
  38. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.collision_test_marginal line 568
  39. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.cutoff_test_integrals line 601
  40. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.collision_test_integrable_of_marginal line 637
  41. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.collisionJump_mass line 693
  42. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.collisionJump_momentum line 699
  43. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.collisionJump_energy line 709
  44. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.collisionJump_log_maxwellian line 737
  45. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.collisionJump_log_density line 746
  46. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.collisionJump_scatter line 757
  47. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.integral_jump_post line 796
  48. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.collisionJump_integrable line 807
  49. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.cutoff_production_identity line 853
  50. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.entropy_production_nonneg line 873
  51. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.cutoff_entropy_nonpositive line 902