OAI/MathematicalPhysics/Boltzmann/Branching/GainNonnegative.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Positivity and domination for the original gain integral

  1. def OAI.BoltzmannNonuniqueness.GainOrder.integrand line 17
  2. theorem OAI.BoltzmannNonuniqueness.GainOrder.integrand_nonneg line 20
  3. theorem OAI.BoltzmannNonuniqueness.GainOrder.integrand_mono line 24
  4. theorem OAI.BoltzmannNonuniqueness.GainOrder.integrand_measurable line 30
  5. theorem OAI.BoltzmannNonuniqueness.GainOrder.integrable_of_le line 43
  6. theorem OAI.BoltzmannNonuniqueness.GainOrder.gain_mono line 52
  7. theorem OAI.BoltzmannNonuniqueness.GainOrder.gain_const_mul line 58
  8. theorem OAI.BoltzmannNonuniqueness.GainOrder.integrable_const_mul line 66
  9. theorem OAI.BoltzmannNonuniqueness.GainOrder.integrable_normalizedGaussian line 74
  10. theorem OAI.BoltzmannNonuniqueness.GainNonnegative.self_eq_lintegral line 105
  11. theorem OAI.BoltzmannNonuniqueness.GainNonnegative.integrable_of_bound line 124
  12. theorem OAI.BoltzmannNonuniqueness.GainNonnegative.gain_le_of_bound line 134