OAI/MathematicalPhysics/Boltzmann/Compactness/PairBoundedTruncation.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

The physical linear gain operator on incoming pair densities

  1. def OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.pairPreRate line 19
  2. def OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.pairPostRate line 23
  3. def OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.pairGain line 26
  4. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.pairPostRate_scatter line 31
  5. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.pairPreRate_measurable line 37
  6. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.pairGain_measurable line 44
  7. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.pairGain_integrable line 49
  8. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.pairGain_test line 62
  9. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.pairGain_eLpNorm_le line 123
  10. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.pairGain_sub_ae line 138
  11. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.pairGain_difference_eLpNorm_le line 155
  12. def OAI.BoltzmannNonuniqueness.CollisionCompactness.relativeCutoff line 189
  13. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.relativeCutoff_measurable line 192
  14. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.relativeCutoff_gaussian_error line 196
  15. def OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.momentPair line 235
  16. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.momentPair_measurable line 238
  17. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.pair_lift_eLpNorm_one line 244
  18. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.pairPreRate_moment_norm_le line 257
  19. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.pairPreRate_integrable_of_moment line 272
  20. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.pairGain_moment_difference_le line 279
  21. def OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.momentVelocityCut line 309
  22. def OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.boundedPairCut line 312
  23. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.incomingBall_measurable line 317
  24. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.boundedPairCut_measurable line 320
  25. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.boundedPairCut_bound line 329
  26. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.boundedPairCut_support line 343
  27. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.boundedPairCut_moment_error line 348