OAI/MathematicalPhysics/Boltzmann/Compactness/PeriodicCharacteristicGainUnit.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The unit-normalized gain bound along every sufficiently late actual subsequence

  1. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.approximatingSolution_subsequence_gain_unit_uniformIntegrable line 20
  2. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.gain_in_measure line 54
  3. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalWeakLimit.global_local_mass line 89
  4. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.gain_discrepancy_L1 line 128
  5. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.loss_residual_L1 line 183
  6. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.characteristic_gain_unit_uniformIntegrable line 229