OAI/MathematicalPhysics/Boltzmann/Compactness/StrongMildRepresentative.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Collision integrability for the strong nonnegative mild representative

  1. theorem OAI.BoltzmannNonuniqueness.kineticDensity_gain line 15
  2. theorem OAI.BoltzmannNonuniqueness.kineticDensity_loss line 21
  3. theorem OAI.BoltzmannNonuniqueness.kineticDensity_collision line 25
  4. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.positiveDensity_measurable line 37
  5. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.positiveDensity_eq_ae line 41
  6. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.positiveDensity_pair_integrable line 47
  7. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.positiveEvolution_strongEarly line 54
  8. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.positiveEvolution_collision_fibers line 77