OAI/MathematicalPhysics/Boltzmann/Compactness/NormalizedPairCompactness.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Factorization of mass-normalized pair moments

  1. theorem OAI.BoltzmannNonuniqueness.Compactness.normalizedPair_moment_identity line 29
  2. theorem OAI.BoltzmannNonuniqueness.Compactness.normalizedPair_moment_limit line 39
  3. theorem OAI.BoltzmannNonuniqueness.Compactness.normalized_pair_eq_of_moments line 107
  4. theorem OAI.BoltzmannNonuniqueness.Compactness.normalizedPair_eq_of_fiber_moments line 136
  5. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.momentPair_normalizedPair line 177
  6. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.momentVelocityCut_normalizedPair line 181
  7. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.normalizedPair_bounded_moment_approximation line 188
  8. theorem OAI.BoltzmannNonuniqueness.Compactness.normalizedPair_product_strong line 241
  9. theorem OAI.BoltzmannNonuniqueness.Compactness.normalizedPair_weak_limit_eq line 298
  10. theorem OAI.BoltzmannNonuniqueness.Compactness.normalizedPair_eq_on_patch line 346
  11. def OAI.BoltzmannNonuniqueness.CollisionCompactness.velocityPairBox line 396
  12. def OAI.BoltzmannNonuniqueness.CollisionCompactness.angularPairBox line 399
  13. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.velocityPairBox_measurable line 402
  14. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.angularPairBox_measurable line 406
  15. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.velocityPairBox_finite line 411
  16. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.weightedPair_angular_local_uniformIntegrable line 420
  17. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.massNormalizedPreRate_local_uniformIntegrable line 442
  18. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.normalizedGain_translation line 470
  19. theorem OAI.BoltzmannNonuniqueness.Compactness.square_identity line 543
  20. theorem OAI.BoltzmannNonuniqueness.Compactness.normalized_average_square_integrable line 550
  21. theorem OAI.BoltzmannNonuniqueness.Compactness.weak_normalized_average_squares line 564
  22. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.normalized_mixed_cutoff_le_chart line 604