OAI/MathematicalPhysics/Boltzmann/Approximation/PositiveIntegralWindow.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Restarting an a.e. mild equation on a bounded time window

  1. def OAI.BoltzmannNonuniqueness.PositiveIntegral.window line 14
  2. theorem OAI.BoltzmannNonuniqueness.PositiveIntegral.measurable_window line 17
  3. theorem OAI.BoltzmannNonuniqueness.PositiveIntegral.window_clamped line 23
  4. theorem OAI.BoltzmannNonuniqueness.PositiveIntegral.window_mild_ae line 30