OAI/MathematicalPhysics/Boltzmann/Branching/ReferenceBranchingHistories.lean

GitHub source file

77 declarations, 0 contain sorry, 0 declared as axioms

Splitting and translating the first-event time integral

  1. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.lintegral_time_split line 17
  2. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.lintegral_time_shift line 27
  3. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.clockSurvival line 58
  4. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.clockDensity line 59
  5. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.clockSurvival_add line 61
  6. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.clockDensity_add line 67
  7. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.advanceState_time_cut line 79
  8. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.finishFlight_time_cut line 89
  9. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.first_event_tail line 96
  10. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.flightFamily_time_cut line 113
  11. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.lintegral_time_triangle line 144
  12. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.renewal_solution_comparison line 213
  13. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.renewal_solution_unique line 266
  14. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.flightFamily_average_bound line 293
  15. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.advanceState_add_remaining line 305
  16. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.flightFamily_add_average line 313
  17. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.flightKernel_add line 343
  18. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.growthWeight line 374
  19. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.growthDensity line 375
  20. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.growthWeight_measurable line 377
  21. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.growthDensity_measurable line 381
  22. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.growthWeight_add line 385
  23. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.growthDensity_integral line 391
  24. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.growthWeight_split line 413
  25. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.weighted_time_cut line 436
  26. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.weightedFlight line 501
  27. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.weightedFlight_measurable line 505
  28. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.clockDensity_eq line 509
  29. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.growthDensity_eq line 513
  30. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.weightedFlight_first_event line 517
  31. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.eventAfterWait line 588
  32. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.rawEventStep line 593
  33. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.eventAfterWait_isSFinite line 596
  34. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.rawEventStep_isSFinite line 599
  35. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.eventDensity line 602
  36. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.eventDensity_measurable line 605
  37. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.eventStep line 609
  38. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.eventStep_isSFinite line 613
  39. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.rawEventStep_lintegral line 620
  40. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.eventStep_lintegral line 635
  41. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.eventStep_pow_isSFinite line 649
  42. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.clockSurvival_le_one line 676
  43. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.eventStep_power_mass_bound line 681
  44. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.eventStep_time_support line 715
  45. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.eventStep_power_time_support line 734
  46. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.eventStep_bounded_remainder line 750
  47. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.eventHistory line 795
  48. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.eventHistory_measurable line 799
  49. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.event_finite_expansion line 803
  50. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.event_subsolution_le_series line 833
  51. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.referenceClock line 865
  52. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.referenceGrowth line 866
  53. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.branchingKernel_mass_bound line 868
  54. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.flightSeed line 881
  55. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.flightSeed_measurable line 884
  56. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.weightedFlight_branching_subsolution line 891
  57. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.weightedFlight_le_branching_series line 930
  58. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.referenceJump_intensity line 968
  59. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.branchingKernel_projection line 987
  60. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.branchingKernel_beam_projection line 1000
  61. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.relative_speed_lipschitz line 1023
  62. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.weighted_speed_error line 1030
  63. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.beam_gain_rate_error line 1047
  64. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumFrequency line 1055
  65. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.medium_frequency_error line 1058
  66. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.flightWeight_secondMoment_le line 1096
  67. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.flightWeight_secondMoment_sum_le line 1118
  68. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.finitePosition line 1152
  69. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.finite_position_error line 1155
  70. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.product_error_bound line 1176
  71. abbrev OAI.BoltzmannNonuniqueness.ReferenceGeometry.HistoryMark line 1222
  72. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.markedChild line 1224
  73. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.markedRate line 1227
  74. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.marked_child_error line 1231
  75. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.markedVelocity line 1242
  76. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.marked_velocity_error line 1247
  77. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.marked_rate_error line 1259