OAI/MathematicalPhysics/Boltzmann/Compactness/WeakL1ToWeakStar.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

The weak-star cold / strong-L1 hot product passage

  1. def OAI.BoltzmannNonuniqueness.Compactness.WeakStarLInfConverges line 23
  2. theorem OAI.BoltzmannNonuniqueness.Compactness.WeakStarLInfConverges.strong_product line 28
  3. theorem OAI.BoltzmannNonuniqueness.Compactness.pairing_restrict_error line 93
  4. theorem OAI.BoltzmannNonuniqueness.Compactness.weakStar_of_exhaustion line 107
  5. theorem OAI.BoltzmannNonuniqueness.Compactness.bounded_pairing_error line 158
  6. theorem OAI.BoltzmannNonuniqueness.Compactness.weakStar_of_continuous_compact_tests line 187
  7. theorem OAI.BoltzmannNonuniqueness.Compactness.weakStar_zero_of_fibers line 235
  8. theorem OAI.BoltzmannNonuniqueness.Published.WeakL1Converges.varying_bounded_mul line 279
  9. theorem OAI.BoltzmannNonuniqueness.Compactness.WeakStarLInfConverges.comp_measurableEquiv line 318
  10. theorem OAI.BoltzmannNonuniqueness.Compactness.WeakStarLInfConverges.restrict line 349
  11. theorem OAI.BoltzmannNonuniqueness.Published.weak_pair_moment_factorization line 382
  12. theorem OAI.BoltzmannNonuniqueness.Published.productionDual_integral_tendsto line 453
  13. theorem OAI.BoltzmannNonuniqueness.Published.ofReal_integral_le_lintegral line 477
  14. theorem OAI.BoltzmannNonuniqueness.Published.weak_production_liminf line 482
  15. theorem OAI.BoltzmannNonuniqueness.Published.WeakL1Converges.weakStar line 532