OAI/MathematicalPhysics/Boltzmann/Branching/SpacetimeRelativeEntropy.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Integrating a uniform entropy budget over a bounded time window

  1. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.spacetimeEntropy line 15
  2. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.spacetimeEntropy_measurable line 18
  3. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.spacetimeEntropy_integrable line 22
  4. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.spacetimeEntropy_integral_le line 43
  5. theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.spacetime_resolvent line 69
  6. theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.velocity_averages_resolvent line 99
  7. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.spacetimeRelativeEntropy line 130
  8. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.spacetimeRelativeEntropy_measurable line 133
  9. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.density_integrable_of_spacetimeEntropy line 140
  10. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.relativeEntropy_integrable_of_spacetimeEntropy line 150
  11. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.spacetimeEntropy_integrable_of_relativeEntropy line 162
  12. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.spacetimeRelativeEntropy_integral_le line 176