OAI/MathematicalPhysics/Boltzmann/Compactness/WeakTimeSurvival.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Measurable local majorants pass to weak L1 limits

  1. theorem OAI.BoltzmannNonuniqueness.Published.WeakL1Converges.le_measurable line 15
  2. theorem OAI.BoltzmannNonuniqueness.Published.WeakL1Converges.le_on_measurable line 38
  3. theorem OAI.BoltzmannNonuniqueness.Published.WeakL1Converges.comp_measurableEquiv line 64
  4. theorem OAI.BoltzmannNonuniqueness.Published.weakL1_affine line 92
  5. theorem OAI.BoltzmannNonuniqueness.Published.WeakL1Converges.le_affine line 110
  6. theorem OAI.BoltzmannNonuniqueness.Published.WeakL1Converges.velocity_moment line 140
  7. theorem OAI.BoltzmannNonuniqueness.WeakTime.ae_survival_of_weak_balance line 184