OAI/MathematicalPhysics/Boltzmann/Approximation/PositiveMildRepresentative.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A nonnegative strongly continuous representative with the exact initial trace

  1. def OAI.BoltzmannNonuniqueness.MildCollisionSolution.positiveEvolution line 14
  2. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.evolution_measurable line 19
  3. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.positiveEvolution_measurable line 25
  4. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.positiveEvolution_nonnegative line 29
  5. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.positiveEvolution_eq_ae line 32
  6. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.positiveEvolution_initial line 40
  7. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.positiveEvolution_strong_continuity line 44
  8. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.positiveEvolution_integrable line 58