OAI/MathematicalPhysics/Boltzmann/Branching/NormalOutgoingSymmetry.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The actual normal-angle law is half the uniform sphere area measure

  1. theorem OAI.BoltzmannNonuniqueness.normalReflection_neg line 16
  2. theorem OAI.BoltzmannNonuniqueness.normalReflection_split line 20
  3. theorem OAI.BoltzmannNonuniqueness.normalReflectionLaw_north line 32
  4. theorem OAI.BoltzmannNonuniqueness.normalReflectionLaw_uniform line 50
  5. theorem OAI.BoltzmannNonuniqueness.normal_left_integral_of_direction line 78
  6. theorem OAI.BoltzmannNonuniqueness.normal_left_integral line 109
  7. theorem OAI.BoltzmannNonuniqueness.outgoing_lintegral line 120
  8. theorem OAI.BoltzmannNonuniqueness.normal_left_integral_outgoing line 126
  9. theorem OAI.BoltzmannNonuniqueness.scatterRight_eq_left_swap line 154
  10. theorem OAI.BoltzmannNonuniqueness.collisionKernel_swap line 160
  11. theorem OAI.BoltzmannNonuniqueness.child_swap line 165
  12. theorem OAI.BoltzmannNonuniqueness.outgoing_swap line 169
  13. theorem OAI.BoltzmannNonuniqueness.normal_right_integral_outgoing line 175