OAI/MathematicalPhysics/Boltzmann/Approximation/PositiveIntegralBound.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Scalar characteristic representatives for a.e. mild solutions

  1. theorem OAI.BoltzmannNonuniqueness.PositiveIntegral.ae_path_bound_of_slices line 15
  2. theorem OAI.BoltzmannNonuniqueness.PositiveIntegral.ae_characteristic_path line 32
  3. theorem OAI.BoltzmannNonuniqueness.PositiveIntegral.ofReal_integral_le line 87
  4. theorem OAI.BoltzmannNonuniqueness.PositiveIntegral.ofReal_add_intervalIntegral_le line 101