OAI/MathematicalPhysics/Boltzmann/Compactness/PeriodicDensityStrong.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The actual positive source bound on one common observation window

  1. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.clipped_positive_survival line 23
  2. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.collisionComparisonError_along line 98
  3. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.positive_comparison_error line 125
  4. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.comparison_error_L1 line 151
  5. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.characteristic_error_L1 line 201
  6. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.positive_difference_L1 line 239
  7. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.density_pair_L1 line 316
  8. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.density_strong line 368