OAI/MathematicalPhysics/Boltzmann/Compactness/UniformIntegrability.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Bounded measurable multipliers preserve uniform integrability

  1. theorem OAI.BoltzmannNonuniqueness.Compactness.uniformIntegrable_of_bounded_multiplier line 18
  2. theorem OAI.BoltzmannNonuniqueness.Compactness.uniformIntegrable_of_varying_multiplier line 62
  3. theorem OAI.BoltzmannNonuniqueness.Compactness.uniformIntegrable_sub line 81
  4. theorem OAI.BoltzmannNonuniqueness.Compactness.tendsto_L1_mul_uniformIntegrable line 105
  5. theorem OAI.BoltzmannNonuniqueness.Compactness.uniformIntegrable_of_approximation line 184
  6. theorem OAI.BoltzmannNonuniqueness.Compactness.uniformIntegrable_indicator_of_restrict line 236
  7. theorem OAI.BoltzmannNonuniqueness.Compactness.uniformIntegrable_add line 270
  8. theorem OAI.BoltzmannNonuniqueness.Compactness.uniformIntegrable_abs_le line 279
  9. theorem OAI.BoltzmannNonuniqueness.Compactness.uniformIntegrable_of_comp_measurePreserving line 307
  10. def OAI.BoltzmannNonuniqueness.Compactness.zeroPrefix line 349
  11. theorem OAI.BoltzmannNonuniqueness.Compactness.zeroPrefix_eventually line 352
  12. theorem OAI.BoltzmannNonuniqueness.Compactness.uniformIntegrable_zeroPrefix line 357
  13. theorem OAI.BoltzmannNonuniqueness.Compactness.eLpNorm_mul_prod_one line 392
  14. theorem OAI.BoltzmannNonuniqueness.Compactness.uniformIntegrable_tensor line 408
  15. theorem OAI.BoltzmannNonuniqueness.Compactness.uniform_min_truncation line 476