OAI/MathematicalPhysics/Boltzmann/Compactness/UniformIntegrableGainTail.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Uniformly integrable families admit bounded truncations without spatial tightness

  1. theorem OAI.BoltzmannNonuniqueness.Published.uniform_value_truncation line 20
  2. theorem OAI.BoltzmannNonuniqueness.Published.uniform_L1_bounded_truncation line 65
  3. theorem OAI.BoltzmannNonuniqueness.Compactness.uniformIntegrable_integral_of_support line 112
  4. theorem OAI.BoltzmannNonuniqueness.Compactness.uniformIntegrable_of_logarithmic_tail line 145