OAI/MathematicalPhysics/Boltzmann/Compactness/PhysicalGainStrictTime.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Almost every finite physical history stays in its explicit reachable region

  1. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.finiteFlightCone_wait line 15
  2. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalWaitingKernel_ae_finiteCone line 32
  3. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalBeamCollision_ae_finiteCone line 48
  4. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalBeamEvent_ae_finiteCone line 74
  5. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalBeamCollision_ae_fixed line 98
  6. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalWaitingKernel_ae_remaining line 113
  7. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalBeamEvent_ae_time_window line 129