OAI/MathematicalPhysics/Boltzmann/Branching/BoundedEntryPortion.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Every nonempty physical history strictly advances collision time

  1. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedDensityScaledEvent_ae_strict_time line 18
  2. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedBoundedDensityScaledEvent_ae_time_window line 39
  3. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.entryPhasePortion line 61
  4. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.entryPhasePortion_measurable line 64
  5. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.entryPhasePortion_union line 68
  6. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.exists_positive_entryPortion line 79
  7. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.entryPhasePortion_cutoff line 86
  8. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.entryPhasePortion_eventually_lateBox line 94
  9. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.positive_entryPortion_eventually_lateBox line 105