OAI/MathematicalPhysics/Boltzmann/Branching/TightApproximation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform L¹ approximation preserves tightness on infinite measure spaces

  1. theorem OAI.BoltzmannNonuniqueness.Compactness.unifTight_of_approximation line 17
  2. theorem OAI.BoltzmannNonuniqueness.Compactness.unifTight_mono line 36
  3. theorem OAI.BoltzmannNonuniqueness.Compactness.unifTight_of_integrable_majorant line 49
  4. theorem OAI.BoltzmannNonuniqueness.Compactness.unifTight_of_spatial_cutoffs line 56