OAI/MathematicalPhysics/Boltzmann/Collision/CollisionConservation.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

An L1 density bound on a fixed elastic collision window

  1. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.windowPartner line 26
  2. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.windowPartner_measurable line 29
  3. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.windowPartner_integrable line 32
  4. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.singleDensity_window_norm_le line 39
  5. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.mem_collisionWindow_scatter line 86
  6. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.mem_collisionWindow_particleSwap line 93
  7. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.windowSingleDensity line 99
  8. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.windowDensitySum line 103
  9. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.windowSingleDensity_measurable line 109
  10. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.windowDensitySum_measurable line 114
  11. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.windowDensitySum_eq line 120
  12. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.four_add_norm_le line 156
  13. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.windowDensitySum_norm_le line 172
  14. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.full_test_collision_invariant line 217
  15. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.energy_collision_balance line 230
  16. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.coordinate_abs_le_energy line 240
  17. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.momentum_rate_integrable line 245
  18. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.momentum_collision_balance line 274
  19. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.collisionAttenuation_window_L1 line 301
  20. def OAI.BoltzmannNonuniqueness.CollisionCompactness.rateDissipation line 361
  21. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.cutoffExtendedProduction_eq_rates line 366
  22. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.rateDissipation_le_liminf_cutoff line 378
  23. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.collisionAttenuation_preRate_L1 line 426
  24. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.base_test_collision_zero line 497