OAI/MathematicalPhysics/Boltzmann/Branching/ReferenceCollisionGeometry.lean

GitHub source file

115 declarations, 0 contain sorry, 0 declared as axioms

The hard-sphere offspring sphere and reference collision rate

The one-child sphere law gives geometric identities for conservation of momentum and energy, and bounds for the two-beam collision frequency.

  1. abbrev OAI.BoltzmannNonuniqueness.ReferenceGeometry.V line 38
  2. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.child line 41

    Source documentation

    One child on the sphere having the two incident velocities as diameter endpoints.

    def child (v w n : V) : V := (1 / 2 : ℝ) • (v + w) + (‖v - w‖ / 2) • n

    Mentions: OAI.BoltzmannNonuniqueness.ReferenceGeometry.V

  3. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.child_distance_center line 43
  4. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.child_pair_sum line 48
  5. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.child_energy line 52
  6. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.child_pair_energy line 63
  7. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.child_energy_le_total line 68
  8. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.energyRadius line 74

    Source documentation

    The radius of the squared-speed interval appearing in the uniform sphere law.

    def energyRadius (v w : V) : ℝ := ‖v - w‖ * ‖v + w‖

    Mentions: OAI.BoltzmannNonuniqueness.ReferenceGeometry.V

  9. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.energyRadius_nonneg line 76
  10. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.energyRadius_le line 80
  11. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.energyRadius_sq line 89

    Source documentation

    The interval-radius formula for a unit cold partner; this is independent of its sign.

    theorem energyRadius_sq (v e : V) (he : ‖e‖ = 1) :
    energyRadius v e ^ 2 = (‖v‖ ^ 2 + 1) ^ 2 - 4 * inner ℝ v e ^ 2 := by
…

    Mentions: OAI.BoltzmannNonuniqueness.ReferenceGeometry.V, OAI.BoltzmannNonuniqueness.ReferenceGeometry.energyRadius

  12. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.two_beam_distance_lower line 95
  13. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.two_beam_distance_upper line 102
  14. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.frequency line 110

    Source documentation

    Collision frequency of a particle in the two unit-strength reference beams.

    def frequency (v e : V) : ℝ := 2 * Real.pi * (‖v - e‖ + ‖v + e‖)

    Mentions: OAI.BoltzmannNonuniqueness.ReferenceGeometry.V

  15. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.frequency_lower line 112
  16. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.frequency_upper line 119
  17. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.child_neg line 140
  18. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.child_lipschitz line 144
  19. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.finite_path_error line 163
  20. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.sphereProbability line 196
  21. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.sphereProbability_isProbability line 198
  22. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.child_measurable line 203
  23. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.outgoing line 208
  24. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.outgoing_isMarkov line 212
  25. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.outgoing_apply line 215
  26. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.outgoing_integral line 223
  27. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.outgoing_energy_support line 227
  28. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.plusProbability line 255
  29. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.plusProbability_mem line 257
  30. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.plusKernel line 262
  31. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.minusKernel line 265
  32. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.plusKernel_isMarkov line 268
  33. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.minusKernel_isMarkov line 272
  34. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.referenceJump line 276
  35. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.plusProbability_measurable line 280
  36. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.referenceJump_isMarkov line 284
  37. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.minusProbability_eq line 300
  38. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.referenceRegion line 324
  39. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.referenceRegion_measurable line 326
  40. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.retention line 329
  41. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.retention_measurable line 331
  42. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.retention_le_one line 334
  43. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.retention_ne_top line 337
  44. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.retainedJump line 340
  45. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.retainedJump_apply line 344
  46. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.retainedJump_univ line 350
  47. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.retainedJump_region line 356
  48. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.retainedJump_rate_identity line 364

    Source documentation

    Each collision rate times its conditional jump law recovers the retained branching rate.

    theorem retainedJump_rate_identity (e v : V) (c : ℝ≥0∞) (hp : retention e v ≠ 0) :
    (c*retention e v) • retainedJump e v = c • (referenceJump e v).restrict referenceRegion := by
…

    Mentions: OAI.BoltzmannNonuniqueness.ReferenceGeometry.V, OAI.BoltzmannNonuniqueness.ReferenceGeometry.retention, OAI.BoltzmannNonuniqueness.ReferenceGeometry.retainedJump, OAI.BoltzmannNonuniqueness.ReferenceGeometry.referenceJump, OAI.BoltzmannNonuniqueness.ReferenceGeometry.referenceRegion

  49. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.retainedRate line 369
  50. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.retainedPotential line 371
  51. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.retention_toReal_mem line 373
  52. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.retainedRate_nonneg line 378
  53. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.retainedRate_le line 382
  54. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.retainedPotential_ge line 391
  55. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.retainedRate_measure_identity line 400
  56. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.exists_small_child line 428
  57. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.child_angular_distance line 454
  58. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.small_child_neighborhood line 462
  59. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.sphere_inner_integrable line 492
  60. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.sphere_inner_integral line 500
  61. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.sphere_abs_inner_integral line 510
  62. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.sphere_abs_inner_integrable line 517
  63. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.sphere_positive_inner_integral line 521
  64. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.outgoing_escape_coarse line 553
  65. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.outgoing_retention_coarse line 601
  66. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.referenceJump_real line 624
  67. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.retention_coarse line 646
  68. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.retention_ne_zero_coarse line 656
  69. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.retainedPotential_coarse line 663
  70. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.smallEntryMass line 690
  71. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.smallEntryMass_pos line 692
  72. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.sphere_small_ball_lower line 695
  73. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.outgoing_small_entry line 714
  74. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.reference_small_entry line 726
  75. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.retained_small_entry line 735
  76. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.referenceJump_measure line 771
  77. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.outgoing_small_region line 782
  78. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.retention_small line 795
  79. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.retainedJump_small line 803
  80. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.two_beam_distance_upper_small line 810
  81. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.plusProbability_lower_small line 817
  82. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.minusProbability_lower_small line 825
  83. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.sphereProbability_neg line 850
  84. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.outgoing_neg line 854
  85. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.plusProbability_neg line 863
  86. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.referenceJump_neg line 872
  87. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.referenceRegion_neg_preimage line 882
  88. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.retention_neg line 886
  89. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.retainedJump_neg line 891
  90. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.sphereRotation line 917
  91. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.sphereRotation_cone line 925
  92. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.sphereRotation_area line 940
  93. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.sphereRotation_probability line 948
  94. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.child_curve_derivative line 970
  95. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.firstAxis line 1005
  96. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.secondAxis line 1006
  97. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.beamAxis line 1007
  98. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.minorizationNormal line 1008
  99. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.axis_norms line 1010
  100. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.first_beam_inner line 1013
  101. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.first_beam_norms line 1016
  102. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.minorizationNormal_norm line 1028
  103. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.minorization_child_zero line 1033
  104. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.minorization_velocity_derivative line 1040
  105. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.sphereCapMass line 1080
  106. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.sphereCapMass_pos line 1082
  107. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.sphere_cap_lower line 1085
  108. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.child_normalized_endpoints line 1103
  109. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.outgoing_endpoint_cap line 1115
  110. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.normalize_curve_derivative line 1149
  111. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.normalize_fderiv line 1166
  112. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.lipschitz_volume_image_le line 1201
  113. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.antilipschitzOn_volume_image_le line 1235
  114. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.minorizationDirections line 1267
  115. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.minorizationDirections_independent line 1271