OAI/MathematicalPhysics/Boltzmann/Branching/MixedRealGain.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Real symmetric mixed gain and its nonnegative bounds

  1. def OAI.BoltzmannNonuniqueness.MixedRealGain.integrand line 14
  2. def OAI.BoltzmannNonuniqueness.MixedRealGain.gain line 19
  3. theorem OAI.BoltzmannNonuniqueness.MixedRealGain.integrand_nonneg line 22
  4. theorem OAI.BoltzmannNonuniqueness.MixedRealGain.integrand_measurable line 28
  5. theorem OAI.BoltzmannNonuniqueness.MixedRealGain.integrand_symm line 41
  6. theorem OAI.BoltzmannNonuniqueness.MixedRealGain.gain_symm line 44
  7. theorem OAI.BoltzmannNonuniqueness.MixedRealGain.gain_eq_symmetricGain line 50
  8. theorem OAI.BoltzmannNonuniqueness.MixedRealGain.gain_self line 53
  9. theorem OAI.BoltzmannNonuniqueness.MixedRealGain.nonnegative_eq_lintegral line 57
  10. theorem OAI.BoltzmannNonuniqueness.MixedRealGain.integrable_of_bound line 73
  11. theorem OAI.BoltzmannNonuniqueness.MixedRealGain.gain_le_of_bound line 82
  12. theorem OAI.BoltzmannNonuniqueness.MixedRealGain.integrand_mono line 94
  13. theorem OAI.BoltzmannNonuniqueness.MixedRealGain.integrable_of_le line 102
  14. theorem OAI.BoltzmannNonuniqueness.MixedRealGain.gain_mono line 113
  15. theorem OAI.BoltzmannNonuniqueness.MixedRealGain.gain_const_mul_right line 119
  16. theorem OAI.BoltzmannNonuniqueness.MixedRealGain.integrable_const_mul_right line 128