OAI/MathematicalPhysics/Boltzmann/Compactness/UniformIntegrableCoordinates.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A vanishing uniform bound controls the integral on a finite measure space

  1. theorem OAI.BoltzmannNonuniqueness.integral_abs_tendsto_of_uniform_bound line 16
  2. theorem OAI.BoltzmannNonuniqueness.Published.eLpNorm_comp_equiv_restrict line 52
  3. theorem OAI.BoltzmannNonuniqueness.Published.uniformIntegrable_comp_equiv line 60
  4. theorem OAI.BoltzmannNonuniqueness.Published.uniformIntegrable_norm_domination line 78