OAI/MathematicalPhysics/Boltzmann/Branching/NonnegativeGainCongruence.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Integrating a nonnegative characteristic source from fiber bounds

  1. theorem OAI.BoltzmannNonuniqueness.integrable_nonnegative_of_fiber_bound line 16
  2. theorem OAI.BoltzmannNonuniqueness.nonnegativeGain_congr_ae line 49