OAI/MathematicalPhysics/Boltzmann/Branching/ReferenceFlightLaws.lean

GitHub source file

109 declarations, 0 contain sorry, 0 declared as axioms

A finite collision-chart measure with a volume lower bound

  1. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.minorizationChart_measurable line 20
  2. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.minorizationChart_measure_lower line 24
  3. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.uniformized_odd_decay line 63
  4. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.uniformized_velocity_mean_decay line 92
  5. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.uniformized_geometric_mean line 118
  6. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.countKernel line 165
  7. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.countKernel_isMarkov line 169
  8. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.poissonKernel line 175
  9. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.poissonKernel_apply line 179
  10. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.poissonKernel_isMarkov line 187
  11. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.poissonKernel_average line 194
  12. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.poisson_power_integral line 224
  13. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.poisson_velocity_mean_decay line 244
  14. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.velocitySum line 282
  15. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.velocitySum_measurable line 285
  16. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.velocitySum_bound line 289
  17. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.velocitySum_succ line 296
  18. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.velocitySum_uniform_bound line 311
  19. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.poissonKernel_lintegral line 343
  20. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.poissonKernel_apply_set line 349
  21. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.poissonKernel_add line 354
  22. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.poissonJoint line 399
  23. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.poissonJoint_isProbability line 402
  24. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.state_inner_bound line 408
  25. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.poissonJoint_inner line 415
  26. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.poisson_velocity_correlation_decay line 431
  27. abbrev OAI.BoltzmannNonuniqueness.ReferenceGeometry.FlightState line 468
  28. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.freeFlight line 470
  29. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.freeFlight_measurable line 472
  30. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.freeFlightKernel line 476
  31. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.freeFlightKernel_isMarkov line 479
  32. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.flightJump line 482
  33. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.flightJump_isMarkov line 486
  34. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.flightJump_apply line 490
  35. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.freeFlightKernel_add line 498
  36. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.freeFlightKernel_zero line 509
  37. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.flightJump_velocity line 515
  38. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.freeFlight_velocity line 523
  39. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.freeFlight_displacement line 530
  40. abbrev OAI.BoltzmannNonuniqueness.ReferenceGeometry.TimeFlightState line 553
  41. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.waitingDensity line 555
  42. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.waitingDensity_measurable line 557
  43. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.waitingTime line 563
  44. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.waitingTime_isSFinite line 566
  45. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.waitingTime_apply line 571
  46. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.waitingTime_mass line 575
  47. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.advanceState line 578
  48. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.advanceState_measurable line 581
  49. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.jumpAfterWait line 586
  50. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.jumpAfterWait_isMarkov line 590
  51. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.historyStep line 593
  52. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.historyStep_isSFinite line 596
  53. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.jumpAfterWait_lintegral line 598
  54. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.historyStep_lintegral line 607
  55. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.finishFlight line 633
  56. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.finishFlight_measurable line 635
  57. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.historyStep_pow_isSFinite line 637
  58. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.historyKernel line 647
  59. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.historyKernel_isSFinite line 650
  60. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.historyKernel_zero line 654
  61. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.historyKernel_succ_lintegral line 659
  62. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.simplexTime line 699
  63. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.simplexTime_ne_top line 701
  64. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.simplexTime_zero line 703
  65. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.simplexTime_integral line 705
  66. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.simplexVolume line 741
  67. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.simplexVolume_nonneg line 743
  68. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.simplexTime_toReal line 747
  69. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.simplexVolume_continuous line 751
  70. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.simplexVolume_step line 755
  71. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.integral_simplexVolume line 760
  72. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.integral_time_simplexVolume line 768
  73. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.integral_time_sq_simplexVolume line 783
  74. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.historyKernel_velocity_lintegral line 817
  75. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.historyKernel_velocity_map line 846
  76. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.historyKernel_mass line 857
  77. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.flightWeight line 879
  78. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.flightWeight_simplexTime line 882
  79. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.flightKernel line 889
  80. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.flightKernel_isSFinite line 894
  81. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.flightKernel_apply line 905
  82. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.flightKernel_velocity_lintegral line 913
  83. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.flightKernel_isMarkov line 925
  84. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.flightKernel_velocity_map line 932
  85. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.realFlightWeight line 961
  86. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.flightFamily line 964
  87. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.flightFamily_isSFinite line 968
  88. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.realFlightWeight_measurable line 977
  89. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.flightFamily_apply line 982
  90. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.flightFamily_eq line 989
  91. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.flightFamily_lintegral line 994
  92. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.realFlightWeight_succ line 1000
  93. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.weighted_history_succ_lintegral line 1035
  94. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.flightFamily_first_event line 1051
  95. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.renewalDensity line 1113
  96. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.renewalDensity_measurable line 1116
  97. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.renewalStep line 1120
  98. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.renewalStep_isSFinite line 1123
  99. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.renewalStep_lintegral line 1129
  100. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.renewalStep_le line 1145
  101. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.flightFamily_renewal line 1160
  102. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.renewalStep_pow_isSFinite line 1185
  103. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.renewalStep_power_le line 1194
  104. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.historyStep_power_mass line 1219
  105. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.renewalStep_power_mass_bound line 1225
  106. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.renewalStep_remainder_tendsto line 1235
  107. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.historyStep_time_support line 1261
  108. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.renewalStep_time_support line 1277
  109. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.renewalStep_power_time_support line 1281