OAI/MathematicalPhysics/Boltzmann/Compactness/WeakLinearMomentLimit.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Weak L¹ compactness for the countably generated kinetic measure spaces

Uniform integrability and tightness give uniformly accurate, bounded finite-window truncations. A common weak L² subsequence has truncation limits that are Cauchy in L¹. Bounded measurable tests then pass to their strong L¹ limit.

  1. theorem OAI.BoltzmannNonuniqueness.Published.l1WeakCompactnessInput line 23
  2. theorem OAI.BoltzmannNonuniqueness.Published.WeakL1Converges.of_L1_approximations line 74
  3. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.weak_linearMoment line 118