OAI/MathematicalPhysics/Boltzmann/Compactness/WeakL1Operations.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

Weak subsequences for the L² truncations used in weak L¹ compactness

  1. theorem OAI.BoltzmannNonuniqueness.Published.exists_weak_L2_subsequence line 29
  2. theorem OAI.BoltzmannNonuniqueness.Published.exists_common_weak_L2_subsequence line 67
  3. def OAI.BoltzmannNonuniqueness.Published.l2Restrict line 113
  4. theorem OAI.BoltzmannNonuniqueness.Published.l2Restrict_ae line 116
  5. theorem OAI.BoltzmannNonuniqueness.Published.weak_L2_limit_support line 120
  6. theorem OAI.BoltzmannNonuniqueness.Published.L2_integrable_of_support line 150
  7. theorem OAI.BoltzmannNonuniqueness.Published.bounded_supported_L2 line 161
  8. theorem OAI.BoltzmannNonuniqueness.Published.weak_L2_bounded_tests line 195
  9. theorem OAI.BoltzmannNonuniqueness.Published.weak_L2_L1_bound line 222
  10. def OAI.BoltzmannNonuniqueness.Published.WeakL1Converges line 290
  11. def OAI.BoltzmannNonuniqueness.Published.L1WeakCompactnessInput line 295
  12. def OAI.BoltzmannNonuniqueness.Published.DunfordPettis1940Theorem321 line 302

    Source documentation

    Only the two kinetic measure spaces needed in the limit construction.

    def DunfordPettis1940Theorem321 : Prop :=
…
  13. theorem OAI.BoltzmannNonuniqueness.Published.WeakL1Converges.comp line 309
  14. theorem OAI.BoltzmannNonuniqueness.Published.WeakL1Converges.nonneg line 314
  15. theorem OAI.BoltzmannNonuniqueness.Published.WeakL1Converges.of_integral_abs_sub line 351
  16. theorem OAI.BoltzmannNonuniqueness.Published.WeakL1Converges.of_eLpNorm_sub line 394
  17. theorem OAI.BoltzmannNonuniqueness.Published.integral_test_marginal line 428
  18. theorem OAI.BoltzmannNonuniqueness.Published.WeakL1Converges.marginal line 444
  19. theorem OAI.BoltzmannNonuniqueness.Published.WeakL1Converges.eq_of_strong line 466
  20. theorem OAI.BoltzmannNonuniqueness.Published.L1WeakCompactnessInput.countable line 510
  21. theorem OAI.BoltzmannNonuniqueness.Published.WeakL1Converges.bounded_mul line 586
  22. theorem OAI.BoltzmannNonuniqueness.Published.WeakL1Converges.unique line 601
  23. theorem OAI.BoltzmannNonuniqueness.Published.WeakL1Converges.congr_limit line 620
  24. theorem OAI.BoltzmannNonuniqueness.Published.WeakL1Converges.sub line 649
  25. theorem OAI.BoltzmannNonuniqueness.Published.WeakL1Converges.congr_sequence line 665
  26. theorem OAI.BoltzmannNonuniqueness.Published.indicator_test_integral line 694
  27. theorem OAI.BoltzmannNonuniqueness.Published.WeakL1Converges.moving_tail line 700
  28. theorem OAI.BoltzmannNonuniqueness.Published.WeakL1Converges.prod_of_fibers line 760
  29. theorem OAI.BoltzmannNonuniqueness.Published.WeakL1Converges.nonnegative_zero_L1 line 813
  30. theorem OAI.BoltzmannNonuniqueness.Published.WeakL1Converges.nonnegative_zero_inMeasure line 833
  31. theorem OAI.BoltzmannNonuniqueness.Published.WeakL1Converges.restrict line 859
  32. theorem OAI.BoltzmannNonuniqueness.Published.WeakL1Converges.restrict_base line 880
  33. theorem OAI.BoltzmannNonuniqueness.Published.WeakL1Converges.vanishing_scalar line 906
  34. theorem OAI.BoltzmannNonuniqueness.Published.WeakL1Converges.withDensity_bounded line 948
  35. theorem OAI.BoltzmannNonuniqueness.Published.integral_comp_measurePreserving line 995
  36. theorem OAI.BoltzmannNonuniqueness.Published.WeakL1Converges.of_comp_measurePreserving line 1002
  37. theorem OAI.BoltzmannNonuniqueness.Published.WeakL1Converges.marginal_eventually line 1037
  38. theorem OAI.BoltzmannNonuniqueness.Published.WeakL1Converges.eq_of_strong_eventually line 1049
  39. theorem OAI.BoltzmannNonuniqueness.Published.WeakL1Converges.prod_constant line 1077
  40. def OAI.BoltzmannNonuniqueness.Published.timeExchange line 1117
  41. theorem OAI.BoltzmannNonuniqueness.Published.timeExchange_apply line 1122
  42. theorem OAI.BoltzmannNonuniqueness.Published.timeExchange_involutive line 1125
  43. theorem OAI.BoltzmannNonuniqueness.Published.timeExchange_measurePreserving line 1127
  44. def OAI.BoltzmannNonuniqueness.Published.timePrimitive line 1133
  45. theorem OAI.BoltzmannNonuniqueness.Published.WeakL1Converges.timePrimitive line 1136
  46. theorem OAI.BoltzmannNonuniqueness.timePositionVolume_restrict line 1183
  47. theorem OAI.BoltzmannNonuniqueness.timePositionVolume_mono line 1190
  48. theorem OAI.BoltzmannNonuniqueness.Published.WeakL1Converges.restrict_time line 1199
  49. theorem OAI.BoltzmannNonuniqueness.Published.WeakL1Converges.le line 1227
  50. theorem OAI.BoltzmannNonuniqueness.Published.WeakL1Converges.le_on line 1237
  51. theorem OAI.BoltzmannNonuniqueness.Published.WeakL1Converges.ge_eventually line 1266
  52. theorem OAI.BoltzmannNonuniqueness.Published.WeakL1Converges.zeroExtension line 1296