OAI/MathematicalPhysics/Boltzmann/Collision/SphereIsometryMeasure.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Orthogonal changes of coordinates preserve the actual sphere area measure

  1. def OAI.BoltzmannNonuniqueness.sphereIsometry line 14
  2. theorem OAI.BoltzmannNonuniqueness.sphereIsometry_cone line 24
  3. theorem OAI.BoltzmannNonuniqueness.sphereIsometry_measurePreserving line 45