OAI/MathematicalPhysics/Boltzmann/Approximation/CutoffLossFrequency.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The cutoff collision terms are dominated by the physical collision marginals

  1. def OAI.BoltzmannNonuniqueness.CollisionCompactness.cutoffLossDensity line 21
  2. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.cutoffLossDensity_measurable line 25
  3. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.cutoffLossDensity_nonneg line 39
  4. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.cutoffGainDensity_nonneg line 45
  5. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.cutoff_gainLoss_le line 50
  6. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.cutoff_gainLoss_uniformIntegrable line 80
  7. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.cutoff_hot_gain_bound line 120
  8. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.normalized_cutoff_hot_gain_bound line 135
  9. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.quadratic_hot_error_tendsto_zero line 144
  10. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.integral_cutoffKernel line 169
  11. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.cutoffLossDensity_eq_frequency line 178
  12. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.cutoff_loss_ae_eq_frequency line 196