OAI/MathematicalPhysics/Boltzmann/Approximation/PositiveComparisonBound.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Exact entropy dissipation for positive bounded cutoff densities

  1. def OAI.BoltzmannNonuniqueness.CollisionCompactness.positiveCutoffProduction line 23
  2. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.positiveCutoffProduction_nonneg line 29
  3. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.cutoff_relative_entropy_identity line 35
  4. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.bounded_positive_entropy_identity line 55
  5. theorem OAI.BoltzmannNonuniqueness.Compactness.positiveDifference_L1 line 122
  6. theorem OAI.BoltzmannNonuniqueness.TransportPrimitive.inv_lipschitzOn_one line 187
  7. theorem OAI.BoltzmannNonuniqueness.TransportPrimitive.positiveDifference_absolutelyContinuous line 199
  8. theorem OAI.BoltzmannNonuniqueness.TransportPrimitive.positiveDifference_hasDerivAt line 213
  9. theorem OAI.BoltzmannNonuniqueness.TransportPrimitive.positiveDifference_evolution line 219
  10. theorem OAI.BoltzmannNonuniqueness.TransportPrimitive.positiveDifference_stability line 241
  11. theorem OAI.BoltzmannNonuniqueness.TransportPrimitive.positiveComparison_integrable line 277
  12. theorem OAI.BoltzmannNonuniqueness.TransportPrimitive.positiveComparison_error_integrable line 314
  13. theorem OAI.BoltzmannNonuniqueness.TransportPrimitive.positiveDifference_error_bound line 352