OAI/MathematicalPhysics/Boltzmann/Approximation/CutoffEntropyMeasure.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The extended nonnegative cutoff dissipation agrees with positive production

  1. def OAI.BoltzmannNonuniqueness.CollisionCompactness.cutoffExtendedProduction line 16
  2. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.positiveCutoffProduction_formula line 26
  3. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.ofReal_positiveCutoffProduction line 45
  4. def OAI.BoltzmannNonuniqueness.CollisionCompactness.cutoffExtendedDissipation line 69
  5. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.ofReal_integral_positiveCutoffProduction line 73