OAI/MathematicalPhysics/Boltzmann/Branching/ReferenceMinorization.lean

GitHub source file

81 declarations, 0 contain sorry, 0 declared as axioms

The physical two-collision law bounds the small four-angle window

  1. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.familyWindow_subset line 22
  2. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.familyWindowMap_le line 32
  3. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.twoCollisionLaw_volume_domination line 72
  4. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.familyWindowAngles line 126
  5. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.familyWindowAngles_measurable line 129
  6. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.firstAngleSet line 133
  7. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.firstAngleSet_measurable line 136
  8. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.localTwoCollisionLaw line 141
  9. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.familyWindowAngles_le line 144
  10. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.familyWindowAngles_mem line 175
  11. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.familyWindowMap_local_le line 189
  12. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.beamEntryMass line 229
  13. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.beamEntryMass_pos line 231
  14. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.reference_beam_entry line 234
  15. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.retained_beam_entry line 280
  16. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.retained_transverse_entry_local line 321
  17. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.retained_two_transverse_entry line 342
  18. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.outgoing_plus_le_retained line 391
  19. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.outgoing_minus_le_retained line 407
  20. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.localCollisionCore_jump_bound line 423
  21. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.localTwoCollisionLaw_apply line 445
  22. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.localTwoCollisionLaw_le_retained line 472
  23. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.retained_two_volume_domination line 513
  24. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.retained_three_volume_domination line 577
  25. abbrev OAI.BoltzmannNonuniqueness.ReferenceGeometry.RetainedState line 641
  26. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.retainedState_norm line 643
  27. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.stateKernel line 646
  28. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.stateKernel_isMarkov line 650
  29. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.stateKernel_apply line 656
  30. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.stateKernel_map line 659
  31. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.stateKernel_integral line 668
  32. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.stateRate line 691
  33. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.jumpFraction line 693
  34. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.stateRate_measurable line 695
  35. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.stateRate_bounds line 700
  36. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.jumpFraction_measurable line 707
  37. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.jumpFraction_bounds line 709
  38. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.uniformizedKernel line 717
  39. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.uniformizedKernel_apply line 721
  40. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.uniformizedKernel_isMarkov line 732
  41. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.uniformizedKernel_lower line 742
  42. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.stateFrequency line 768
  43. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.statePotential line 770
  44. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.stateFrequency_measurable line 772
  45. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.statePotential_lower line 776
  46. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.stateFrequency_bounds line 779
  47. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.branchingKernel line 784
  48. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.branchingKernel_isSFinite line 788
  49. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.branchingKernel_apply line 802
  50. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.uniformizedKernel_intensity line 813
  51. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.branchingKernel_decomposition line 825
  52. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.branchingKernel_lower line 836
  53. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.stateKernel_map_kernel line 863
  54. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.stateKernel_pow_map line 868
  55. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.stateBallMeasure line 887
  56. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.state_three_volume_domination line 890
  57. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.stateNeg line 933
  58. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.stateNeg_val line 945
  59. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.stateKernel_neg line 947
  60. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.frequency_neg line 955
  61. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.stateRate_neg line 961
  62. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.jumpFraction_neg line 964
  63. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.uniformizedKernel_neg line 967
  64. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.stateBallMeasure_map line 973
  65. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.volume_ball_neg line 981
  66. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.stateBallMeasure_neg line 990
  67. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.stateKernel_power_le_uniformized line 1014
  68. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.uniformized_three_volume_domination line 1040
  69. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.uniformizedKernel_pow_isMarkov line 1072
  70. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.stateBallMeasure_univ line 1082
  71. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.uniformized_common_part line 1088
  72. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.state_odd_integral_zero line 1140
  73. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.integral_common_part_bound line 1151
  74. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.uniformized_three_odd_contraction line 1170
  75. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.chainAverage line 1202
  76. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.uniformizedKernel_pow_neg line 1205
  77. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.chainAverage_measurable line 1223
  78. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.chainAverage_odd line 1226
  79. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.chainAverage_bound line 1237
  80. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.chainAverage_zero line 1242
  81. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.chainAverage_add line 1247