OAI/MathematicalPhysics/Boltzmann/Approximation/CapHotTransportBalance.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

The concrete outer-annulus bound for the positive cap family

  1. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.outer_bound line 30
  2. theorem OAI.BoltzmannNonuniqueness.TransportCutoff.kineticWindow_velocity_integrable line 71
  3. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.localized_hot_sources_ui_tail line 85
  4. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.average_limit_identified line 145
  5. structure OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairExtraction line 201
  6. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.exists_hot_pair_extraction line 207
  7. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.exists_hot_pair_limit line 224
  8. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.eventually_hot_average_bounded line 256
  9. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.hot_resolvent_averaging line 310
  10. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.hot_averages_compact line 363
  11. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.hot_countable_averages_compact line 426
  12. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.strong_averages line 501
  13. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.moment_bound line 555
  14. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CompactCapFamily.weak_limit_moment line 580
  15. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.eventually_transport_test_integrable line 628
  16. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.hot_characteristic_test line 683
  17. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.eventually_hot_transport_balance line 723