OAI/MathematicalPhysics/Boltzmann/Compactness/PairPatchIdentity.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Strong L1 continuity of translations on the outgoing velocity-pair space

  1. def OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.pairTranslation line 25
  2. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.pairTranslation_continuous line 28
  3. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.pairTranslation_preserving line 31
  4. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.pair_translation_L1 line 35
  5. def OAI.BoltzmannNonuniqueness.Compactness.pairTestAverage line 72
  6. theorem OAI.BoltzmannNonuniqueness.Compactness.pairTestAverage_integrable line 76
  7. theorem OAI.BoltzmannNonuniqueness.Compactness.pairTestAverage_add line 82
  8. theorem OAI.BoltzmannNonuniqueness.Compactness.pairTestAverage_smul line 95
  9. theorem OAI.BoltzmannNonuniqueness.Compactness.pair_tests_determine line 117
  10. theorem OAI.BoltzmannNonuniqueness.Compactness.pairTestAverage_uniform_error line 175
  11. theorem OAI.BoltzmannNonuniqueness.Compactness.pair_eq_product_of_moments line 216
  12. theorem OAI.BoltzmannNonuniqueness.Compactness.unscale_pair_moment line 277
  13. theorem OAI.BoltzmannNonuniqueness.Compactness.pair_identity_on_patch line 297