OAI/MathematicalPhysics/Boltzmann/Approximation/CapLimitTransport.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

The physical hot collision decomposition on each compact time cylinder

  1. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.eventually_hot_collision_identity line 35
  2. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.loss_measure_compact_limit line 88
  3. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.eventually_hot_source_error_identity line 143
  4. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.hot_source_weak_limit line 190
  5. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.gain_measure_separated_limit line 279
  6. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.gain_measure_compact_limit line 330
  7. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.separated_transport_balance line 390
  8. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.hot_source_compact_limit line 477
  9. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.transport_measure_balance line 571
  10. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.hot_periodic line 650
  11. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.euclideanHot_div_weight line 674
  12. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.boundedHotRatio_periodic line 682
  13. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.attenuated_transport_balance line 727
  14. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.separated_transport_measure_balance line 803
  15. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.characteristic_test_balance line 867
  16. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.characteristicGainMeasure line 924
  17. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.characteristicLossMeasure line 930
  18. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.characteristic_cumulative_balance line 936
  19. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.covered_characteristic_weak_balance line 1014
  20. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.characteristicGain_test_integral line 1098
  21. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.characteristicGain_normal_integral line 1126
  22. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction.common_characteristic_weak_balance line 1166
  23. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.characteristicGain_hot_integral line 1236