OAI/MathematicalPhysics/Boltzmann/Branching/ThreeCollisionTimes.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Positive three-collision access from a bounded incoming velocity

  1. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.three_collision_access_positive line 18
  2. abbrev OAI.BoltzmannNonuniqueness.ReferenceGeometry.ThreeWaits line 87
  3. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.threeWaitBox line 89
  4. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.threeWaitBox_measurable line 92
  5. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.threeWaitBox_volume line 95
  6. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.threeWaitBox_sum line 102
  7. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.threeWaitBox_integral_pos line 107
  8. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.three_wait_survival line 117