OAI/MathematicalPhysics/Boltzmann/Compactness/KineticEntropyErrorLimit.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Integrable entropy tests for bounded kinetic densities

  1. theorem OAI.BoltzmannNonuniqueness.kinetic_log_product_integrable line 19
  2. theorem OAI.BoltzmannNonuniqueness.kinetic_log_integral_bound line 60
  3. def OAI.BoltzmannNonuniqueness.gaussianRegularizedDensity line 100
  4. theorem OAI.BoltzmannNonuniqueness.gaussianRegularizedDensity_measurable line 103
  5. theorem OAI.BoltzmannNonuniqueness.kinetic_regularization_error_bound line 108
  6. theorem OAI.BoltzmannNonuniqueness.kinetic_regularization_entropy_integrable line 130
  7. theorem OAI.BoltzmannNonuniqueness.kinetic_entropy_error_tendsto line 171