OAI/MathematicalPhysics/Boltzmann/Approximation/MildConservation.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Integrable local mass tests and cancellation of their collision source

  1. def OAI.BoltzmannNonuniqueness.massTestIntegrand line 25
  2. theorem OAI.BoltzmannNonuniqueness.MassTest.slice_integrable line 29
  3. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.mass_source_integrable line 42
  4. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.mass_source_zero line 53
  5. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.mass_integrand_integrable line 87
  6. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.massTestIntegrand_along_eq line 114
  7. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.mass_balance_with_source line 127
  8. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.local_mass_balance line 165
  9. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.local_mass_of_terminal_zero line 181
  10. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.energy_source_zero line 209
  11. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.energy_characteristic_integrable line 231
  12. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.energy_characteristic_zero line 250
  13. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.energy_conservation line 259
  14. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.entropy_admissible line 301
  15. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.coordinate_source_zero line 374
  16. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.coordinate_characteristic_integrable line 399
  17. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.coordinate_conservation line 412
  18. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.momentum_conservation line 438