OAI/MathematicalPhysics/Boltzmann/Collision/VelocitySmoothingError.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Smooth compact velocity cutoffs preserving a prescribed test

  1. theorem OAI.BoltzmannNonuniqueness.Compactness.exists_velocity_cutoff line 19
  2. def OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.velocityShift line 45
  3. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.velocityShift_preserving line 53
  4. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.velocityShift_test line 57
  5. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.velocityShift_difference_test line 65
  6. def OAI.BoltzmannNonuniqueness.Compactness.velocityExhaustionBump line 101
  7. def OAI.BoltzmannNonuniqueness.Compactness.velocityExhaustion line 104
  8. theorem OAI.BoltzmannNonuniqueness.Compactness.velocityExhaustion_smooth line 106
  9. theorem OAI.BoltzmannNonuniqueness.Compactness.velocityExhaustion_compact line 109
  10. theorem OAI.BoltzmannNonuniqueness.Compactness.velocityExhaustion_nonneg line 112
  11. theorem OAI.BoltzmannNonuniqueness.Compactness.velocityExhaustion_le_one line 115
  12. theorem OAI.BoltzmannNonuniqueness.Compactness.velocityExhaustion_eq_one line 118
  13. theorem OAI.BoltzmannNonuniqueness.Compactness.velocityExhaustion_error_tendsto line 123
  14. def OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.parameterShift line 147
  15. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.parameterShift_measurable line 150
  16. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.parameterShift_preserving line 153
  17. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.integrable_velocity_kernel line 167
  18. theorem OAI.BoltzmannNonuniqueness.Published.velocity_spectral_bound line 190
  19. def OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.velocitySmooth line 234
  20. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.velocitySmooth_integrable line 237
  21. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.velocitySmooth_difference line 242
  22. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.velocitySmooth_error_le line 256