OAI/MathematicalPhysics/Boltzmann/Branching/NormalGainMeasureActions.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

The actual normal-angle gain kernel for measurable cold partner measures

  1. def OAI.BoltzmannNonuniqueness.normalChild line 21
  2. theorem OAI.BoltzmannNonuniqueness.normalChild_measurable line 24
  3. def OAI.BoltzmannNonuniqueness.normalParameters line 27
  4. def OAI.BoltzmannNonuniqueness.normalRate line 30
  5. theorem OAI.BoltzmannNonuniqueness.normalRate_measurable line 33
  6. def OAI.BoltzmannNonuniqueness.normalChildKernel line 37
  7. instance OAI.BoltzmannNonuniqueness.normalParameters_sFinite line 41
  8. instance OAI.BoltzmannNonuniqueness.normalChildKernel_sFinite line 44
  9. theorem OAI.BoltzmannNonuniqueness.normalChildKernel_lintegral line 52
  10. def OAI.BoltzmannNonuniqueness.normalGainKernel line 73
  11. instance OAI.BoltzmannNonuniqueness.normalGainKernel_sFinite line 76
  12. theorem OAI.BoltzmannNonuniqueness.normalGainKernel_lintegral line 79
  13. def OAI.BoltzmannNonuniqueness.normalPhaseGainKernel line 109
  14. instance OAI.BoltzmannNonuniqueness.normalPhaseGainKernel_sFinite line 112
  15. theorem OAI.BoltzmannNonuniqueness.normalPhaseGainKernel_lintegral line 117
  16. theorem OAI.BoltzmannNonuniqueness.normalReflectionVector_isometry line 149
  17. theorem OAI.BoltzmannNonuniqueness.normalReflection_isometry line 154
  18. def OAI.BoltzmannNonuniqueness.normalReflectionLaw line 160
  19. theorem OAI.BoltzmannNonuniqueness.normalReflectionLaw_lintegral line 164
  20. theorem OAI.BoltzmannNonuniqueness.normalReflectionLaw_isometry line 172
  21. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.incomingCollisionMeasure_lintegral line 216
  22. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.normalPhaseGain_comp line 228
  23. theorem OAI.BoltzmannNonuniqueness.normalGainKernel_eq_smul_of_measure_eq line 289
  24. theorem OAI.BoltzmannNonuniqueness.normalPhaseGainKernel_lintegral_gain line 299