OAI/MathematicalPhysics/Boltzmann/Branching/RadialReflectionChangeVariables.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

A polynomial radial extension of the normal-angle reflection map

On the positive hemisphere this quadratic map is injective. Its radial coordinate is squared, allowing the angular change of variables to be proved in ambient space.

  1. def OAI.BoltzmannNonuniqueness.radialReflection line 19
  2. theorem OAI.BoltzmannNonuniqueness.radialReflection_continuous line 22
  3. theorem OAI.BoltzmannNonuniqueness.radialReflection_inner line 26
  4. theorem OAI.BoltzmannNonuniqueness.radialReflection_norm line 33
  5. theorem OAI.BoltzmannNonuniqueness.radialReflection_sphere line 42
  6. theorem OAI.BoltzmannNonuniqueness.radialReflection_injOn line 49
  7. theorem OAI.BoltzmannNonuniqueness.radialReflection_image line 83
  8. def OAI.BoltzmannNonuniqueness.radialReflectionDerivative line 142
  9. theorem OAI.BoltzmannNonuniqueness.radialReflection_hasFDerivAt line 146
  10. def OAI.BoltzmannNonuniqueness.northSphere line 153
  11. theorem OAI.BoltzmannNonuniqueness.radialReflectionDerivative_north line 156
  12. theorem OAI.BoltzmannNonuniqueness.radialReflectionDerivative_det_north line 166
  13. theorem OAI.BoltzmannNonuniqueness.radialReflection_image_ae line 198
  14. theorem OAI.BoltzmannNonuniqueness.lintegral_radialReflection_north line 230