OAI/MathematicalPhysics/Boltzmann/Approximation/CapMixedCollisionLimits.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

The actual cap family has a positive limit with its full collision terms

  1. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.TightCapFamily.exists_collision_limit line 31
  2. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.cold_spacetime_weakStar_limit line 78
  3. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.physicalCollisionError line 146
  4. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.physicalCollisionError_measurable line 151
  5. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.vanishing_physical_collision_error line 159
  6. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.mixedDensity line 216
  7. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.mixedDensity_measurable line 219
  8. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.mixedDensity_nonneg line 228
  9. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.mixedDensity_integrable line 235
  10. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.mixedPrelimitMeasure line 265
  11. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.mixedPrelimitMeasure_finite line 269
  12. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.mixed_average_weak_limit line 300
  13. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.mixedPrelimitMeasure_gaussian_moment line 380
  14. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.eventually_mixedPrelimitMeasure_gaussian_bound line 422
  15. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.mixedPrelimitMeasure_integral line 479
  16. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.mixedPrelimitMeasure_tensor line 489
  17. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.mixed_tensor_integrable line 511
  18. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.mixed_measure_tensor_limit line 550
  19. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.mixed_measure_compact_limit line 622
  20. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.mixed_measure_linear_growth_limit line 683
  21. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.collisionCutoff line 742
  22. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.collisionCutoff_tendsto line 744
  23. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.mixed_relative_cutoff_limit line 749
  24. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.mixed_incoming_collision_limit line 800
  25. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.eventually_mixedPreRate_integrable line 851
  26. def OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.physicalCold line 890
  27. def OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.physicalHot line 894
  28. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.physical_hot_collision line 898
  29. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.physicalGainMeasure line 943
  30. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.physicalLossMeasure line 948
  31. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.eventually_physicalCollisionMeasures_finite line 953
  32. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.mixed_physical_loss_limit line 990
  33. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.mixed_physical_gain_limit line 1073
  34. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.collisionDilation line 1138
  35. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.rescaledColdDensity_eq_physical line 1142
  36. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.physicalHotDensity_eq_physical line 1150
  37. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.rescaled_hot_collision line 1158
  38. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.loss_measure_separated_limit line 1207