OAI/MathematicalPhysics/Boltzmann/Compactness/PhysicalEvolution.lean

GitHub source file

79 declarations, 0 contain sorry, 0 declared as axioms

The actual global density equals its nonlinear characteristic profile

  1. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.linear_profile_eq_density_local line 33
  2. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.linear_profile_eq_density line 56
  3. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.linear_entropy_bound_ae_on_window line 90
  4. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.linear_entropy_bound_ae line 112
  5. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.linear_entropy_bound line 140
  6. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.linear_finiteEntropy line 158
  7. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.physicalEntropyBudget line 191
  8. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.linear_relativeEntropy_le line 196
  9. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.linear_entropyMoment_le line 207
  10. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.linear_joint_entropy_ae line 237
  11. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.linear_joint_entropy line 267
  12. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.linear_profile_strong_seq line 305
  13. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.linear_profile_strong_continuous line 329
  14. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.physicalEvolution line 358
  15. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.physicalEvolution_measurable line 361
  16. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.physicalEvolution_nonneg line 369
  17. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.physicalEvolution_initial line 372
  18. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.physicalEvolution_along line 377
  19. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.physicalEvolution_eq_density line 384
  20. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.physicalEvolution_eq line 418
  21. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.physical_finiteEntropy line 424
  22. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.physical_entropyMoment_le line 436
  23. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.physical_strong_continuous line 452
  24. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalAdvance line 488
  25. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalAdvance_measurable line 491
  26. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalWaitingWeight line 496
  27. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalWaitingWeight_measurable line 500
  28. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalWaitingKernel line 507
  29. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalWaitingKernel_sFinite line 511
  30. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalWaitingKernel_lintegral line 523
  31. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.physical_weak_seq line 560
  32. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.physical_linearMoment_weak_seq line 576
  33. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.physical_linear_test_seq line 597
  34. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalMarkedCollision line 636
  35. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalMarkedCollision_sFinite line 642
  36. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalMarkedCollision_velocity_integral line 647
  37. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalMarkedCollision_lintegral line 660
  38. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalMarkedEvent line 671
  39. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalMarkedEvent_sFinite line 675
  40. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalMarkedEvent_lintegral line 680
  41. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumMarkedKernel_le line 714
  42. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalMarkedCollision_le line 726
  43. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalMarkedEvent_le line 738
  44. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalMarkedWord line 743
  45. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalMarkedWord_sFinite line 748
  46. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalMarkedWord_le line 756
  47. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalMarkedWord_step line 766
  48. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalEventMeasure line 794
  49. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalEventMeasure_sFinite line 796
  50. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalParameterWeight line 800
  51. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalParameterWeight_measurable line 805
  52. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalParameterWeight_ne_top line 815
  53. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalMarkedEvent_parameters line 825
  54. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalBeamCollision line 872
  55. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalBeamCollision_sFinite line 876
  56. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalBeamEvent line 881
  57. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalBeamEvent_sFinite line 885
  58. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalMarkedCollision_le_beam line 890
  59. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalMarkedEvent_le_beam line 899
  60. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalMarkedWord_le_beam line 904
  61. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalBeamCollision_lintegral line 915
  62. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalBeamEvent_pow_sFinite line 941
  63. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalGainEndpoint line 949
  64. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalGainEndpoint_sFinite line 954
  65. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalGainEndpoint_lintegral line 962
  66. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalGainEndpoint_apply line 975
  67. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.physical_entropy_dissipation line 998
  68. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.collisionSource_const_mul line 1041
  69. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.collisionSource_base_comp line 1048
  70. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.mixed_source_rescale line 1052
  71. theorem OAI.BoltzmannNonuniqueness.physical_gainLoss_eq line 1075
  72. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.physical_spacetime_entropy line 1108
  73. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.physical_kinetic_entropy line 1120
  74. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.physical_kinetic_dissipation_lt_top line 1128
  75. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.physical_kinetic_collision_integrability line 1144
  76. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.linear_source_eq_physical_collision line 1183
  77. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.physical_weak_continuity line 1228
  78. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.physical_renormalized_field_along line 1263
  79. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.physical_eq_density_ae line 1291