OAI/MathematicalPhysics/Boltzmann/Collision/AxialJointAnalytic.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Spatial derivatives of the implicit cold-jet flow

  1. def OAI.BoltzmannNonuniqueness.AxialDerivative.A line 23
  2. theorem OAI.BoltzmannNonuniqueness.AxialDerivative.A_nonneg line 25
  3. theorem OAI.BoltzmannNonuniqueness.AxialDerivative.profile_derivative line 28
  4. theorem OAI.BoltzmannNonuniqueness.AxialDerivative.characteristic_derivative line 37
  5. theorem OAI.BoltzmannNonuniqueness.AxialDerivative.foot_derivative line 41
  6. theorem OAI.BoltzmannNonuniqueness.AxialDerivative.velocity_derivative line 51
  7. theorem OAI.BoltzmannNonuniqueness.AxialDerivative.velocity_derivative_nonneg line 62
  8. def OAI.BoltzmannNonuniqueness.AxialTransport.flightFoot line 88
  9. def OAI.BoltzmannNonuniqueness.AxialTransport.flightVelocity line 90
  10. theorem OAI.BoltzmannNonuniqueness.AxialTransport.velocity_abs_le line 92
  11. theorem OAI.BoltzmannNonuniqueness.AxialTransport.flightFoot_distance line 99
  12. theorem OAI.BoltzmannNonuniqueness.AxialTransport.flightFoot_continuousAt line 121
  13. theorem OAI.BoltzmannNonuniqueness.AxialFlightDerivative.time_mul_derivative line 156
  14. theorem OAI.BoltzmannNonuniqueness.AxialFlightDerivative.flightFoot_derivative line 167
  15. theorem OAI.BoltzmannNonuniqueness.AxialFlightDerivative.flightVelocity_derivative line 197
  16. theorem OAI.BoltzmannNonuniqueness.AxialFlow.foot_time_space_bound line 228
  17. theorem OAI.BoltzmannNonuniqueness.AxialFlow.foot_joint_continuousAt line 240
  18. theorem OAI.BoltzmannNonuniqueness.AxialFlow.clamped_foot_continuous line 255
  19. theorem OAI.BoltzmannNonuniqueness.AxialFlow.clamped_velocity_continuous line 267
  20. theorem OAI.BoltzmannNonuniqueness.AxialAnalytic.tanh_analytic line 295
  21. theorem OAI.BoltzmannNonuniqueness.AxialAnalytic.profile_analytic line 301
  22. theorem OAI.BoltzmannNonuniqueness.AxialAnalytic.characteristic_analytic line 307
  23. theorem OAI.BoltzmannNonuniqueness.AxialAnalytic.foot_analytic line 311
  24. theorem OAI.BoltzmannNonuniqueness.AxialAnalytic.velocity_analytic line 324
  25. abbrev OAI.BoltzmannNonuniqueness.AxialAnalytic.FlowParameters line 351
  26. def OAI.BoltzmannNonuniqueness.AxialAnalytic.jointCharacteristic line 353
  27. def OAI.BoltzmannNonuniqueness.AxialAnalytic.jointFoot line 356
  28. theorem OAI.BoltzmannNonuniqueness.AxialAnalytic.jointProfile_analytic line 359
  29. theorem OAI.BoltzmannNonuniqueness.AxialAnalytic.jointCharacteristic_analytic line 369
  30. theorem OAI.BoltzmannNonuniqueness.AxialAnalytic.jointCharacteristic_derivative_fst line 376
  31. theorem OAI.BoltzmannNonuniqueness.AxialAnalytic.jointCharacteristic_derivative_vertical line 383
  32. theorem OAI.BoltzmannNonuniqueness.AxialAnalytic.jointFoot_analytic line 393
  33. theorem OAI.BoltzmannNonuniqueness.AxialAnalytic.jointVelocity_analytic line 423