OAI/MathematicalPhysics/Boltzmann/Compactness/StrongPairMoment.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Measurable strong L¹ limits are integrable

  1. theorem OAI.BoltzmannNonuniqueness.Published.integrable_of_strong_limit line 20
  2. theorem OAI.BoltzmannNonuniqueness.Published.WeakL1Converges.eq_of_strong_limit line 31
  3. theorem OAI.BoltzmannNonuniqueness.Compactness.strongL1_of_strong_fibers line 54
  4. theorem OAI.BoltzmannNonuniqueness.Compactness.strong_bounded_product line 91
  5. theorem OAI.BoltzmannNonuniqueness.Compactness.strong_bounded_kernel_averages line 139
  6. theorem OAI.BoltzmannNonuniqueness.Compactness.strong_on_patch_of_weighted line 183
  7. theorem OAI.BoltzmannNonuniqueness.Published.weak_pair_moment_of_strong_product line 225