OAI/MathematicalPhysics/Boltzmann/Approximation/RegularizedEntropyIntegrability.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The finite-approximation entropy-production inequality, with vanishing error

  1. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.bounded_log_source_integrable line 20
  2. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.regularized_entropy_production_bound line 40
  3. theorem OAI.BoltzmannNonuniqueness.regularized_relative_entropy_integrable line 97