OAI/MathematicalPhysics/Boltzmann/Branching/MediumEndpointTransport.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Each marked event is damped free waiting followed by physical collision

  1. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumEventKernel_eq_comp line 21
  2. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumEventKernel_remaining_le line 53
  3. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumEventKernel_pow_eq_comp line 72
  4. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalWaitingKernel_eq_transport line 109
  5. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumCharacteristicKernel line 120
  6. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumCharacteristicKernel_sFinite line 124
  7. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumStateCollision_eq_transport line 129
  8. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumEventKernel_pow_characteristic line 134
  9. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumCharacteristicKernel_lintegral line 145
  10. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumFlightSeed_characteristic line 175
  11. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumEndpointKernel_characteristic line 193