OAI/MathematicalPhysics/Boltzmann/Compactness/LocalizedBlockComparison.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Retaining the actual open-left collision-time window in physical histories

  1. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalCollisionWindow line 19
  2. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalCollisionWindow_measurable line 21
  3. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.localizedNormalWindowEvent line 24
  4. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.localizedNormalWindowEvent_sFinite line 29
  5. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.localizedNormalWindowEvent_transport line 35
  6. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.boundedHistory_le_localized_window line 48
  7. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.localizedNormalWindowEvent_pow_transport line 96
  8. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.localizedNormal_endpoint_characteristic line 105
  9. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.localizedHistoryBlockMass line 143
  10. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalBlock_le_localized line 152