OAI/MathematicalPhysics/Boltzmann/Branching/ReferenceHistoryMoments.lean

GitHub source file

77 declarations, 0 contain sorry, 0 declared as axioms

Measurable extension of retained-state observables to the physical velocity space

  1. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.state_projection_exists line 18
  2. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.stateProjection line 22
  3. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.stateProjection_measurable line 24
  4. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.stateProjection_apply line 27
  5. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.stateProjection_coe line 30
  6. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.branchingKernel_lintegral_physical line 35
  7. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.medium_frequency_bounds line 76
  8. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.marked_rate_bounds line 97
  9. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.markedReferenceWeight line 142
  10. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.markedReferenceState line 146
  11. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.reference_frequency_eq line 149
  12. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.markedReference_integral line 153
  13. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.historyKernel_displacement line 204
  14. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.historyKernel_isFinite line 233
  15. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.history_displacement_integrable line 239
  16. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.history_displacement_sq_integrable line 244
  17. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.product_error_on_range line 268
  18. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.marked_product_error line 285
  19. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.referenceVelocity line 334
  20. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.coupled_velocity_error line 337
  21. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.coupled_velocity_bound line 344
  22. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.coupled_marked_product_error line 359
  23. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.markedChild_measurable line 412
  24. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.markedRate_measurable line 420
  25. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.markedReferenceWeight_measurable line 428
  26. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.markedReferenceState_measurable line 434
  27. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.eventHistory_marked_succ line 438
  28. abbrev OAI.BoltzmannNonuniqueness.ReferenceGeometry.EventParameter line 476
  29. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.eventParameterMeasure line 478
  30. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.eventParameterMeasure_isFinite line 481
  31. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.eventParameterMeasure_mass line 485
  32. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.referenceParameterState line 491
  33. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.referenceParameterDensity line 494
  34. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.referenceParameterState_measurable line 497
  35. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.referenceParameterDensity_measurable line 512
  36. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.reference_parameter_integral line 528
  37. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.eventHistory_parameter_succ line 553
  38. abbrev OAI.BoltzmannNonuniqueness.ReferenceGeometry.MarkedEventParameter line 592
  39. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.markedEventMeasure line 594
  40. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.markedEventMeasure_isFinite line 597
  41. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.markedParameterState line 601
  42. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.markedParameterDensity line 604
  43. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.markedParameterState_measurable line 607
  44. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.markedParameterDensity_measurable line 614
  45. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.markedParameterDensity_ne_top line 621
  46. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.eventHistory_marked_parameter_succ line 632
  47. abbrev OAI.BoltzmannNonuniqueness.ReferenceGeometry.ParameterWord line 664
  48. abbrev OAI.BoltzmannNonuniqueness.ReferenceGeometry.parameterWordMeasurable line 668
  49. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.parameterWordMeasure line 676
  50. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.parameterWordMeasure_isFinite line 680
  51. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.parameterWordState line 688
  52. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.parameterWordDensity line 692
  53. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.parameterWordState_measurable line 697
  54. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.parameterWordDensity_measurable line 709
  55. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.parameterWordDensity_ne_top line 721
  56. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.markedParameterDensity_zero line 744
  57. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.markedParameterState_time line 748
  58. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.eventHistory_zero line 752
  59. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.parameterWord_integral line 758
  60. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.historyKernel_succ line 807
  61. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.jumpAfterWait_apply line 814
  62. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.id_prod_integral line 822
  63. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.historyStep_integral line 829
  64. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.historyKernel_succ_integral line 841
  65. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.historyMean line 868
  66. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.historyMean_shift line 871
  67. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.historyMean_formula line 882
  68. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.historySecondMoment line 945
  69. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.historySecondMoment_shift line 948
  70. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.historyMean_bound line 974
  71. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.historySecondMoment_uniform_bound line 1001
  72. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.flight_displacement_second_moment line 1104
  73. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.flight_displacement_tail line 1156
  74. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.flight_small_displacement line 1183
  75. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.markedEventMeasure_mass line 1228
  76. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.parameterWordMeasure_mass line 1234
  77. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.parameterWordMeasure_mass_ne_top line 1245