OAI/MathematicalPhysics/Boltzmann/Branching/TimeSliceIntegration.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

From almost-everywhere positive-time slices to spacetime bounds

  1. theorem OAI.BoltzmannNonuniqueness.Compactness.ae_interval_of_slices line 13
  2. theorem OAI.BoltzmannNonuniqueness.Compactness.measurableSet_ae_fiber line 25
  3. theorem OAI.BoltzmannNonuniqueness.Compactness.ae_interval_nested_of_slices line 38
  4. theorem OAI.BoltzmannNonuniqueness.VelocityMoment.measurable_moment line 49