OAI/MathematicalPhysics/Boltzmann/Approximation/MassNormalizedCollisionLimits.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Strong spatial masses remove gain normalization in measure

  1. theorem OAI.BoltzmannNonuniqueness.Compactness.tendstoInMeasure_of_strong_massNormalized line 27
  2. theorem OAI.BoltzmannNonuniqueness.MassTest.exists_time_cutoff line 62
  3. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.massRegularizedPreRate line 100
  4. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.massRegularizedPostRate line 104
  5. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.massRegularizedPreRate_measurable line 108
  6. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.massRegularizedPostRate_eq line 114
  7. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.massRegularizedPostRate_measurable line 117
  8. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.massRegularizedPreRate_bounds line 122
  9. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.massRegularizedPreRate_integrable line 135
  10. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.massRegularizedPostRate_integrable line 146
  11. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.massPreRate_velocity_tail line 170
  12. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.collisionMassClip line 228
  13. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.collisionMassClip_measurable line 232
  14. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.collisionMassClip_strong_on_box line 236
  15. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.collisionWindow_subset_angularPairBox line 268
  16. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.collisionMassClip_strong_on_window line 274
  17. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.collisionWindow_mono line 303
  18. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.massRegularizedPreRate_on_window line 309
  19. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.massRegularizedPreRate_window_difference line 319
  20. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.massRegularizedPreRate_window_L1 line 332
  21. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.massRegularizedPreRate_difference_bound line 372
  22. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.massRegularizedPreRate_L1 line 380
  23. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.massRegularizedPostRate_L1 line 428
  24. theorem OAI.BoltzmannNonuniqueness.Compactness.strong_mass_of_velocity_averages line 467
  25. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.weak_massRegularizedPreRate line 518
  26. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.weak_massRegularizedPostRate line 537
  27. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.massRegularized_gain line 572
  28. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.massNormalized_gain line 579
  29. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.massRegularizedGain_L1 line 587
  30. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.massRegularized_loss line 634
  31. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.massNormalized_loss line 641
  32. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.massRegularizedLoss_L1 line 649