OAI/MathematicalPhysics/Boltzmann/Approximation/RegularizedDissipationBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Retaining dissipation in the Gaussian regularization estimate

  1. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.regularized_entropy_dissipation_bound line 17