OAI/MathematicalPhysics/Boltzmann/Compactness/EntropyDissipationAverage.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

The integrable entropy error caused by positive regularization

  1. def OAI.BoltzmannNonuniqueness.entropyErrorCoefficient line 24
  2. theorem OAI.BoltzmannNonuniqueness.entropyErrorCoefficient_nonneg line 28
  3. theorem OAI.BoltzmannNonuniqueness.cutoffCollision_measurable line 34
  4. theorem OAI.BoltzmannNonuniqueness.entropy_regularization_error line 47
  5. def OAI.BoltzmannNonuniqueness.entropyGaussian line 103
  6. theorem OAI.BoltzmannNonuniqueness.entropyGaussian_integrable line 106
  7. theorem OAI.BoltzmannNonuniqueness.entropy_controls_mass_energy line 124
  8. theorem OAI.BoltzmannNonuniqueness.finiteEntropy_of_relativeEntropy_integrable line 130
  9. theorem OAI.BoltzmannNonuniqueness.tendsto_mul_abs_log_zero line 174
  10. theorem OAI.BoltzmannNonuniqueness.tendsto_mul_affine_abs_log_zero line 181
  11. theorem OAI.BoltzmannNonuniqueness.integral_logarithmicMajorant line 191
  12. theorem OAI.BoltzmannNonuniqueness.tendsto_integrated_entropy_error line 210
  13. theorem OAI.BoltzmannNonuniqueness.entropy_dissipation_of_vanishing_error line 240
  14. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.mass_marginal_uniformIntegrable line 280
  15. def OAI.BoltzmannNonuniqueness.entropyMomentCoefficient line 319
  16. theorem OAI.BoltzmannNonuniqueness.entropyMomentCoefficient_nonneg line 322
  17. theorem OAI.BoltzmannNonuniqueness.entropyMoment_control line 326
  18. theorem OAI.BoltzmannNonuniqueness.entropyMoment_integral_control line 360
  19. theorem OAI.BoltzmannNonuniqueness.ennreal_liminf_add_nat line 400
  20. theorem OAI.BoltzmannNonuniqueness.entropy_dissipation_of_liminfs line 411
  21. theorem OAI.BoltzmannNonuniqueness.entropy_dissipation_average_limit line 436