OAI/MathematicalPhysics/Boltzmann/Jets/SpatialCutoffIntegrability.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Removing small spatial regions in the collision-integrability argument

  1. def OAI.BoltzmannNonuniqueness.Compactness.outerCutoff line 17
  2. theorem OAI.BoltzmannNonuniqueness.Compactness.spatial_cutoff_error line 20
  3. theorem OAI.BoltzmannNonuniqueness.Compactness.uniformIntegrable_of_spatial_cutoffs line 46