OAI/MathematicalPhysics/Boltzmann/Collision/AngularPairTests.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Angular normalization of the hard-sphere collision kernel

The angular measure is the ordinary area measure volume.toSphere. Its mass is 4 * π; the absolute normal component integrates to 2 * π * ‖g‖.

  1. instance OAI.BoltzmannNonuniqueness.sphereArea_isFiniteMeasure line 24
  2. theorem OAI.BoltzmannNonuniqueness.sphereArea_real_univ line 28
  3. theorem OAI.BoltzmannNonuniqueness.sphereArea_univ line 37
  4. theorem OAI.BoltzmannNonuniqueness.gaussian_radial_one line 42
  5. theorem OAI.BoltzmannNonuniqueness.gaussian_radial_three line 54
  6. theorem OAI.BoltzmannNonuniqueness.gaussian_abs_integral line 68
  7. theorem OAI.BoltzmannNonuniqueness.gaussian_coordinate_integral line 76
  8. theorem OAI.BoltzmannNonuniqueness.gaussian_linear_integral line 96
  9. theorem OAI.BoltzmannNonuniqueness.gaussian_radial_weighted line 111
  10. theorem OAI.BoltzmannNonuniqueness.gaussian_polar_identity line 125
  11. theorem OAI.BoltzmannNonuniqueness.integrable_abs_inner_sphereArea line 159
  12. theorem OAI.BoltzmannNonuniqueness.integral_abs_inner_sphereArea line 168

    Source documentation

    The normal-parametrized hard-sphere angular integral has coefficient 2 * π.

    theorem integral_abs_inner_sphereArea (g : Velocity) :
    (∫ ω : Sphere, |inner ℝ g (ω : Velocity)| ∂sphereArea) = 2 * Real.pi * ‖g‖ := by
…

    Mentions: OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.Sphere, OAI.BoltzmannNonuniqueness.sphereArea

  13. theorem OAI.BoltzmannNonuniqueness.integral_collisionKernel_sphereArea line 175

    Source documentation

    The loss-frequency angular normalization in the manuscript.

    theorem integral_collisionKernel_sphereArea (v w : Velocity) :
    (∫ ω : Sphere, collisionKernel v w ω ∂sphereArea) = 2 * Real.pi * ‖v - w‖ :=
…

    Mentions: OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.Sphere, OAI.BoltzmannNonuniqueness.collisionKernel, OAI.BoltzmannNonuniqueness.sphereArea

  14. theorem OAI.BoltzmannNonuniqueness.integrable_collisionKernel_sphereArea line 179
  15. def OAI.BoltzmannNonuniqueness.Compactness.angularPostTest line 197
  16. theorem OAI.BoltzmannNonuniqueness.Compactness.angularPostTest_continuous line 200
  17. def OAI.BoltzmannNonuniqueness.Compactness.angularPostCutoffTest line 212
  18. theorem OAI.BoltzmannNonuniqueness.Compactness.angularPostCutoffTest_hasCompactSupport line 217