OAI/MathematicalPhysics/Boltzmann/Branching/MixedPhysicalMeasures.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

Polarized cutoff rates and their exact collision-map symmetries

  1. def OAI.BoltzmannNonuniqueness.CollisionCompactness.mixedPreRate line 23
  2. def OAI.BoltzmannNonuniqueness.CollisionCompactness.mixedPostRate line 27
  3. def OAI.BoltzmannNonuniqueness.CollisionCompactness.mixedGainDensity line 31
  4. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.mixedPreRate_measurable line 37
  5. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.mixedPreRate_particleSwap line 49
  6. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.mixedPostRate_particleSwap line 60
  7. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.mixedPostRate_scatter line 67
  8. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.mixedPostRate_formula line 74
  9. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.integral_mixedPostRate_scatter line 83
  10. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.integral_mixedPostRate_swap line 99
  11. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.mixedPreRate_integrable line 145
  12. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.mixedPostRate_integrable line 159
  13. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.mixedPostRate_test_integrable line 167
  14. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.mixedPreRate_swapped_integrable line 180
  15. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.mixedPreRate_sum_test_integrable line 190
  16. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.mixedPreRate_self line 230
  17. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.mixedPostRate_self line 237
  18. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.mixedPostRate_add_self line 243
  19. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.mixedGainDensity_self line 252
  20. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.cutoffGain_add line 258
  21. def OAI.BoltzmannNonuniqueness.CollisionCompactness.mixedLossDensity line 304
  22. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.mixedLossDensity_eq_frequency line 309
  23. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.mixed_loss_ae_eq_frequency line 326
  24. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.mixed_loss_test_integrable line 337
  25. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.mixedGain_test_identity line 374
  26. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.relativeCutoff_incomingLoss line 433
  27. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.mixed_loss_velocity_integral line 439
  28. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.mixed_pre_angular_integral line 480
  29. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.mixedGain_test_incoming line 499
  30. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.mixed_pre_loss_angular_integral line 546
  31. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.mixedLoss_test_incoming line 559
  32. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.mixedGain_congr_ae line 608
  33. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.mixedPostRate_nonneg line 665
  34. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.mixedPostRate_le_self line 671
  35. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.mixedPostRate_fiber_integrable line 680
  36. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.mixedGainDensity_le_nonnegative line 717
  37. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.mixed_pair_rate_integrable_of_gaussian line 782
  38. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.mixed_gain_test_integrable line 831
  39. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.mixedGainDensity_nonneg line 862
  40. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.mixedLossDensity_nonneg line 871
  41. def OAI.BoltzmannNonuniqueness.CollisionCompactness.mixedGainMeasure line 877
  42. def OAI.BoltzmannNonuniqueness.CollisionCompactness.mixedLossMeasure line 880
  43. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.mixedGainDensity_integrable line 883
  44. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.mixedLossDensity_integrable line 891
  45. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.mixedGainMeasure_finite line 901
  46. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.mixedLossMeasure_finite line 909
  47. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.mixedGainMeasure_integral line 917
  48. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.mixedLossMeasure_integral line 925