OAI/MathematicalPhysics/Boltzmann/Compactness/LocalizedGainCompactness.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Removing velocity smoothing from entropy-controlled localized gains

  1. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.velocitySmooth_error_eLpNorm_le line 15
  2. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.localizedGain_strong_of_smoothing line 24