OAI/MathematicalPhysics/Boltzmann/Compactness/LocalizedGainSmoothingAE.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Incoming-velocity localization of the actual physical gain

  1. def OAI.BoltzmannNonuniqueness.CollisionCompactness.localizedPostRate line 21
  2. def OAI.BoltzmannNonuniqueness.CollisionCompactness.localizedPhysicalGain line 26
  3. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.localizedPostRate_measurable line 30
  4. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.localizedPostRate_integrable line 38
  5. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.localizedPhysicalGain_integrable line 53
  6. def OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.localizedPair line 79
  7. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.localizedPair_preRate line 83
  8. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.localizedPair_postRate line 91
  9. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.localizedPhysicalGain_eq_pairGain line 97
  10. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.exists_velocity_unit_cutoff line 120
  11. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.localizedPair_weight line 131
  12. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.localizedGain_tail_le line 138
  13. def OAI.BoltzmannNonuniqueness.TransportCutoff.localizedSource line 212
  14. theorem OAI.BoltzmannNonuniqueness.TransportCutoff.localizedSource_causal line 215
  15. theorem OAI.BoltzmannNonuniqueness.TransportCutoff.localizedSource_on line 220
  16. theorem OAI.BoltzmannNonuniqueness.TransportCutoff.localizedSource_velocity_support line 224
  17. theorem OAI.BoltzmannNonuniqueness.TransportCutoff.localizedSource_measurable line 233
  18. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.localizedGain_translation line 258
  19. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.localizedPhysicalGain_smoothing line 299
  20. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.collision_rate_fibers line 365
  21. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.localizedPhysicalGain_smoothing_ae line 373