OAI/MathematicalPhysics/Boltzmann/Collision/SphereDirectionAbsolute.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

A measurable direction map with an arbitrary value at zero

  1. def OAI.BoltzmannNonuniqueness.sphereDirection line 15
  2. theorem OAI.BoltzmannNonuniqueness.sphereDirection_measurable line 19
  3. theorem OAI.BoltzmannNonuniqueness.sphereDirection_smul line 30
  4. theorem OAI.BoltzmannNonuniqueness.sphereDirection_radialReflection line 43
  5. def OAI.BoltzmannNonuniqueness.sphereBallLift line 64
  6. theorem OAI.BoltzmannNonuniqueness.sphereBallLift_measurable line 67
  7. theorem OAI.BoltzmannNonuniqueness.sphereBallLift_radial line 72
  8. theorem OAI.BoltzmannNonuniqueness.sphereBallLift_integral line 78
  9. theorem OAI.BoltzmannNonuniqueness.radial_cubic_factor line 94
  10. theorem OAI.BoltzmannNonuniqueness.sphereArea_absolutelyContinuous_directions line 119