OAI/MathematicalPhysics/Boltzmann/Approximation/CapPairMoments.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

A compatible global weak limit for the actual hot pair products

  1. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.pairLimit line 32
  2. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.pairLimit_measurable line 35
  3. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.pairLimit_nonneg line 39
  4. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.pairLimit_eq_local line 42
  5. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.pairLimit_weak line 57
  6. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.subsequence line 68
  7. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.subsequence_pairLimit line 75
  8. def OAI.BoltzmannNonuniqueness.EuclideanFlight.hotPairChart line 95
  9. theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.hotPairChart_measurePreserving line 101
  10. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.physical_pair_weak line 118
  11. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.euclideanHot_pair_eq_chart line 133
  12. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.euclidean_pair_weak line 140
  13. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.euclideanHot_weighted_pair_eq_chart line 172
  14. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.weighted_pair_physical_weak line 179
  15. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.eventually_weighted_pair_integrable line 226
  16. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CompactCapFamily.averaging_subsequence line 266
  17. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.eventually_pair_integrable line 310
  18. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.pair_moment_of_strong line 353
  19. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.averages_resolvent line 408
  20. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CompactCapFamily.physical_averages_subsequence line 425
  21. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CompactCapFamily.countable_physical_averages line 458
  22. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.TightCapFamily.exists_weak_and_average_limits line 490
  23. def OAI.BoltzmannNonuniqueness.JetCopyDatum.averageWeight line 535
  24. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.TightCapFamily.exists_factorized_pair_moments line 538