OAI/MathematicalPhysics/Boltzmann/Collision/CollisionWeakMarginals.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

Integrable velocity majorants for hard-sphere pair densities

  1. def OAI.BoltzmannNonuniqueness.CollisionCompactness.pairKernel line 21
  2. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.pairKernel_nonneg line 24
  3. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.pairKernel_measurable line 27
  4. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.pairKernel_integrable line 31
  5. def OAI.BoltzmannNonuniqueness.CollisionCompactness.pairDensity line 43
  6. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.pairDensity_measurable line 46
  7. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.pairDensity_nonneg line 50
  8. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.pairDensity_bound line 55
  9. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.pair_ae_bound line 85
  10. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.outer_pairs_uniformIntegrable line 113
  11. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.collision_pairs_uniformIntegrable line 145
  12. def OAI.BoltzmannNonuniqueness.CollisionCompactness.scatterTriple line 184
  13. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.scatterTriple_measurable line 188
  14. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.scatterTriple_involutive line 193
  15. def OAI.BoltzmannNonuniqueness.CollisionCompactness.scatterTripleEquiv line 200
  16. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.scatterTriple_measurePreserving line 209
  17. def OAI.BoltzmannNonuniqueness.CollisionCompactness.preRate line 237
  18. def OAI.BoltzmannNonuniqueness.CollisionCompactness.postRate line 240
  19. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.postRate_formula line 245
  20. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.preRate_measurable line 253
  21. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.preRate_nonneg line 258
  22. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.preRate_le_pairDensity line 263
  23. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.preRate_integrable line 269
  24. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.postRate_integrable line 278
  25. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.integral_postRate line 284
  26. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.rates_integrable_of_uniformIntegrable line 290
  27. def OAI.BoltzmannNonuniqueness.CollisionCompactness.collisionGrouping line 322
  28. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.collisionGrouping_measurePreserving line 327
  29. def OAI.BoltzmannNonuniqueness.CollisionCompactness.gainDensity line 343
  30. def OAI.BoltzmannNonuniqueness.CollisionCompactness.lossDensity line 346
  31. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.gainDensity_formula line 349
  32. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.lossDensity_formula line 358
  33. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.gainDensity_nonneg line 363
  34. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.lossDensity_nonneg line 366
  35. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.gainLoss_integrable line 369
  36. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.gainLoss_integral_eq line 386
  37. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.gainDensity_measurable line 435
  38. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.lossDensity_measurable line 440
  39. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.slice_lintegral line 445
  40. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.slice_postRate_mass line 453
  41. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.marginal_mass_le line 468
  42. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.gainLoss_slice_mass_le line 497
  43. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.integral_order_outside line 545
  44. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.gainLoss_order_outside line 559
  45. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.hot_pairDensity_integrable line 581
  46. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.gainLoss_outer_bound line 590
  47. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.uniformIntegrable_mono_nonneg line 627
  48. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.outer_uniformIntegrable line 641
  49. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.outer_gainLoss_uniformIntegrable line 660
  50. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.collision_gainLoss_uniformIntegrable line 682
  51. def OAI.BoltzmannNonuniqueness.CollisionCompactness.normalizedKernel line 731
  52. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.normalizedKernel_measurable line 734
  53. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.normalizedKernel_bound line 739
  54. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.preRate_eq_normalized line 747
  55. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.weak_preRate line 754
  56. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.weak_postRate line 764
  57. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.weak_grouped_rate line 798
  58. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.weak_gainLoss line 812