OAI/MathematicalPhysics/Boltzmann/Approximation/PositiveContributionsIntegrable.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A cutoff equal to one preserves every collision ending in its core

  1. theorem OAI.BoltzmannNonuniqueness.withDensity_restrict_le_of_core line 23
  2. theorem OAI.BoltzmannNonuniqueness.positiveSourceKernel_restrict_le line 34
  3. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.finitePositiveSource line 69
  4. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.physicalPositiveSource line 74
  5. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.positive_source_limit line 79
  6. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.survivingInitial_integrable line 122
  7. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.finitePositiveSource_integrable line 135