OAI/MathematicalPhysics/Boltzmann/Branching/CommonMomentEnvelope.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

A common square-integrable envelope for all capped velocity moments

  1. theorem OAI.BoltzmannNonuniqueness.AnnularEnvelope.squareEnvelope_measurable line 15
  2. def OAI.BoltzmannNonuniqueness.AnnularEnvelope.commonMoment line 18
  3. theorem OAI.BoltzmannNonuniqueness.AnnularEnvelope.commonMoment_measurable line 21
  4. theorem OAI.BoltzmannNonuniqueness.AnnularEnvelope.commonMoment_nonneg line 24
  5. theorem OAI.BoltzmannNonuniqueness.AnnularEnvelope.finiteEnvelope_nonneg line 28
  6. theorem OAI.BoltzmannNonuniqueness.AnnularEnvelope.finiteEnvelope_le_sqrt line 36
  7. theorem OAI.BoltzmannNonuniqueness.AnnularEnvelope.affine_le_commonMoment line 43
  8. theorem OAI.BoltzmannNonuniqueness.AnnularEnvelope.commonMoment_square_le line 48
  9. theorem OAI.BoltzmannNonuniqueness.AnnularEnvelope.torus_common_square_integrable line 55