OAI/MathematicalPhysics/Boltzmann/Collision/VelocityAverageDifference.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Joint integrability for damped velocity-dependent characteristic lines

  1. def OAI.BoltzmannNonuniqueness.Published.velocityLineShear line 12
  2. theorem OAI.BoltzmannNonuniqueness.Published.velocityLineShear_measurePreserving line 15
  3. def OAI.BoltzmannNonuniqueness.Published.velocityTimeShear line 26
  4. theorem OAI.BoltzmannNonuniqueness.Published.velocityTimeShear_measurePreserving line 29
  5. def OAI.BoltzmannNonuniqueness.Published.velocityLineResolvent line 41
  6. theorem OAI.BoltzmannNonuniqueness.Published.velocityLine_integrable line 44
  7. theorem OAI.BoltzmannNonuniqueness.Published.velocityLineResolvent_integrable line 51
  8. def OAI.BoltzmannNonuniqueness.Published.velocityLineAverage line 55
  9. theorem OAI.BoltzmannNonuniqueness.Published.velocityLineAverage_integrable line 58
  10. theorem OAI.BoltzmannNonuniqueness.Published.integral_norm_partial_le line 75
  11. theorem OAI.BoltzmannNonuniqueness.Published.velocityLineShear_integral_norm line 85
  12. theorem OAI.BoltzmannNonuniqueness.Published.velocityLineResolvent_L1_le line 96
  13. theorem OAI.BoltzmannNonuniqueness.Published.velocityLineAverage_L1_le line 111
  14. theorem OAI.BoltzmannNonuniqueness.Published.velocityLineResolvent_sub line 130
  15. theorem OAI.BoltzmannNonuniqueness.Published.velocityLineAverage_sub line 139
  16. theorem OAI.BoltzmannNonuniqueness.Published.velocityLineAverage_eLpNorm_le line 152
  17. theorem OAI.BoltzmannNonuniqueness.Published.velocityLineAverage_difference_le line 161