OAI/MathematicalPhysics/Boltzmann/Compactness/StrongCompactPairTests.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Strong L1 continuity of the time primitive on a finite time window

  1. theorem OAI.BoltzmannNonuniqueness.Published.strong_timePrimitive line 30
  2. theorem OAI.BoltzmannNonuniqueness.StrongEarly.restrict line 81
  3. theorem OAI.BoltzmannNonuniqueness.Published.weakL1_of_eLpNorm_sub line 107
  4. theorem OAI.BoltzmannNonuniqueness.Published.entropy_liminf_of_eLpNorm_sub line 120
  5. def OAI.BoltzmannNonuniqueness.Published.timeSurvival line 145
  6. theorem OAI.BoltzmannNonuniqueness.Published.timeSurvival_measurable line 148
  7. theorem OAI.BoltzmannNonuniqueness.Published.timePrimitive_nonneg line 152
  8. theorem OAI.BoltzmannNonuniqueness.Published.timeSurvival_bounds line 162
  9. theorem OAI.BoltzmannNonuniqueness.Published.strong_timeSurvival line 166
  10. theorem OAI.BoltzmannNonuniqueness.Compactness.strongL1_of_two_sided_approximations line 197
  11. def OAI.BoltzmannNonuniqueness.Published.timeDifference line 241
  12. theorem OAI.BoltzmannNonuniqueness.Published.timeDifference_measurable line 243
  13. theorem OAI.BoltzmannNonuniqueness.Published.strong_timeDifference line 247
  14. def OAI.BoltzmannNonuniqueness.Published.twoTimeSurvival line 279
  15. theorem OAI.BoltzmannNonuniqueness.Published.twoTimeSurvival_bounds line 283
  16. theorem OAI.BoltzmannNonuniqueness.Published.twoTimeSurvival_measurable line 287
  17. theorem OAI.BoltzmannNonuniqueness.Published.strong_twoTimeSurvival line 291
  18. theorem OAI.BoltzmannNonuniqueness.Published.twoTimeSurvival_eq_interval line 317
  19. theorem OAI.BoltzmannNonuniqueness.Compactness.strong_linearMoment_averages line 357
  20. theorem OAI.BoltzmannNonuniqueness.Compactness.strong_of_normalized_second_moments line 429
  21. theorem OAI.BoltzmannNonuniqueness.Compactness.strongL1_add line 468
  22. theorem OAI.BoltzmannNonuniqueness.Compactness.strongL1_const_mul line 482
  23. theorem OAI.BoltzmannNonuniqueness.Compactness.strong_supported_tensor_pair_tests line 507
  24. theorem OAI.BoltzmannNonuniqueness.Compactness.strong_average_of_normalized_pairs line 548
  25. theorem OAI.BoltzmannNonuniqueness.Compactness.strong_compact_pair_tests line 617