OAI/MathematicalPhysics/Boltzmann/Compactness/LocalL1ApproximationLimit.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

The actual gain divided by one plus density is uniformly integrable locally

  1. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.gain_unit_uniformIntegrable_local line 21
  2. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.approximatingSolution_gain_unit_uniformIntegrable_local line 39
  3. theorem OAI.BoltzmannNonuniqueness.Published.localL2_L1_bound line 67
  4. theorem OAI.BoltzmannNonuniqueness.Published.localL2_L1_tendsto line 79
  5. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.physicalLoss_unit_uniformIntegrable_local line 107
  6. theorem OAI.BoltzmannNonuniqueness.Published.local_pair_moment_factorization line 143
  7. theorem OAI.BoltzmannNonuniqueness.Published.lintegral_le_of_closedBall_bounds line 210
  8. theorem OAI.BoltzmannNonuniqueness.Published.localL1_global_bound line 236
  9. theorem OAI.BoltzmannNonuniqueness.Published.localL2_global_L1_bound line 262
  10. theorem OAI.BoltzmannNonuniqueness.Published.eLpNorm_sub_triangle line 290
  11. theorem OAI.BoltzmannNonuniqueness.Published.localL1_difference_tendsto line 296
  12. theorem OAI.BoltzmannNonuniqueness.Published.localL1_approximation_difference_bound line 325
  13. theorem OAI.BoltzmannNonuniqueness.Published.localL1_approximation_cauchy line 342
  14. theorem OAI.BoltzmannNonuniqueness.Published.WeakL1Converges.eq_of_local_strong line 382
  15. theorem OAI.BoltzmannNonuniqueness.Published.LocalL1Converges.congr_on_window line 413
  16. theorem OAI.BoltzmannNonuniqueness.Published.localL1_approximation_limit line 440