OAI/MathematicalPhysics/Boltzmann/Approximation/MildInitialAE.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Initial traces of the a.e. characteristic equations

  1. theorem OAI.BoltzmannNonuniqueness.PositiveIntegral.value_zero line 15
  2. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.MildAE.initial_ae line 24
  3. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.ColdMildAE.initial_ae line 30