OAI/MathematicalPhysics/Boltzmann/Branching/MomentAverageBound.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Cutoff-independent loss frequency from the half-Gaussian moment

  1. theorem OAI.BoltzmannNonuniqueness.VelocityMoment.weighted_integrable line 17
  2. theorem OAI.BoltzmannNonuniqueness.VelocityMoment.weighted_integral_le line 24
  3. theorem OAI.BoltzmannNonuniqueness.VelocityMoment.frequency_le_moment line 34
  4. theorem OAI.BoltzmannNonuniqueness.VelocityMoment.mass_lintegral_le_moment line 86
  5. theorem OAI.BoltzmannNonuniqueness.VelocityMoment.integrable_of_moment_bound line 93
  6. theorem OAI.BoltzmannNonuniqueness.VelocityMoment.integral_le_of_moment_bound line 100
  7. theorem OAI.BoltzmannNonuniqueness.VelocityMoment.average_le_of_moment_bound line 108