OAI/MathematicalPhysics/Boltzmann/Branching/ClippedProductionLimit.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Bounded restoration of spatial mass preserves the dissipation bound

  1. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.extendedProduction_eq_regularized_rates line 21
  2. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.collisionMassClip_ratio_bounds line 33
  3. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.clipped_regularizedProduction_le line 44
  4. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.collisionMassClip_eventually_full line 68
  5. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.weak_clipped_collision_rates line 96
  6. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.clipped_production_liminf line 152