OAI/MathematicalPhysics/Boltzmann/Compactness/NormalizedCollisionRates.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

The first-velocity-moment weight of the normalized pair is integrable

  1. def OAI.BoltzmannNonuniqueness.Compactness.pairVelocityWeight line 20
  2. def OAI.BoltzmannNonuniqueness.Compactness.weightedNormalizedPair line 22
  3. theorem OAI.BoltzmannNonuniqueness.Compactness.pairVelocityWeight_measurable line 25
  4. theorem OAI.BoltzmannNonuniqueness.Compactness.weightedNormalizedPair_measurable line 29
  5. theorem OAI.BoltzmannNonuniqueness.Compactness.normalizedTensor_integrable_swap line 34
  6. theorem OAI.BoltzmannNonuniqueness.Compactness.weightedNormalizedPair_integrable line 43
  7. theorem OAI.BoltzmannNonuniqueness.Compactness.bounded_nonnegative_product_div line 79
  8. theorem OAI.BoltzmannNonuniqueness.Compactness.normalized_entropyTruncation_uniformIntegrable line 87
  9. theorem OAI.BoltzmannNonuniqueness.Compactness.normalizedPair_uniformIntegrable line 134
  10. def OAI.BoltzmannNonuniqueness.Compactness.pairVelocityCut line 183
  11. theorem OAI.BoltzmannNonuniqueness.Compactness.pairVelocityCut_measurable line 186
  12. theorem OAI.BoltzmannNonuniqueness.Compactness.tail_coeff_bound line 192
  13. theorem OAI.BoltzmannNonuniqueness.Compactness.tail_density_nonneg line 200
  14. theorem OAI.BoltzmannNonuniqueness.Compactness.pairVelocityCut_pointwise_error line 210
  15. theorem OAI.BoltzmannNonuniqueness.Compactness.pairVelocityCut_L1_error line 234
  16. def OAI.BoltzmannNonuniqueness.Compactness.boundedPairWeight line 297
  17. theorem OAI.BoltzmannNonuniqueness.Compactness.boundedPairWeight_measurable line 300
  18. theorem OAI.BoltzmannNonuniqueness.Compactness.boundedPairWeight_bound line 307
  19. theorem OAI.BoltzmannNonuniqueness.Compactness.pairVelocityCut_eq_mul line 318
  20. theorem OAI.BoltzmannNonuniqueness.Compactness.weak_weightedNormalizedPair line 324
  21. theorem OAI.BoltzmannNonuniqueness.Compactness.normalizedPair_entropy_error line 381
  22. theorem OAI.BoltzmannNonuniqueness.Compactness.truncated_pair_support line 402
  23. theorem OAI.BoltzmannNonuniqueness.Compactness.normalizedPair_unifTight line 416
  24. def OAI.BoltzmannNonuniqueness.CollisionCompactness.massNormalizedPreRate line 462
  25. def OAI.BoltzmannNonuniqueness.CollisionCompactness.massNormalizedPostRate line 465
  26. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.massNormalizedPreRate_eq line 469
  27. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.massNormalizedPreRate_eq_fun line 476
  28. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.massNormalizedPostRate_eq line 481
  29. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.massNormalizedPreRate_measurable line 484
  30. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.massNormalizedPostRate_measurable line 489
  31. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.massNormalizedPreRate_integrable line 494
  32. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.massNormalizedPostRate_integrable line 501
  33. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.weak_massNormalizedPreRate line 506
  34. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.weak_massNormalizedPostRate line 516