OAI/MathematicalPhysics/Boltzmann/Compactness/LocalMomentIntegrability.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Passing from all compact restrictions to an almost-everywhere assertion

  1. theorem OAI.BoltzmannNonuniqueness.Compactness.ae_of_all_compact_restrict line 19
  2. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.localTwoCollisionLaw_volume_domination line 45
  3. theorem OAI.BoltzmannNonuniqueness.entropyMoment_spacetime_integrable line 105
  4. theorem OAI.BoltzmannNonuniqueness.mass_transport_integrable line 130