OAI/MathematicalPhysics/Boltzmann/Branching/RedundantPlaneIntegral.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

A nonsingular three-dimensional coordinate map for a collision plane

The third coordinate is the coefficient of the normal, rather than distance along the unit normal. This normalization cancels the length of the normal in the redundant-parameter density. The transverse normal must be nonzero, just as in the graph chart used by the actual gain kernel.

  1. abbrev OAI.BoltzmannNonuniqueness.RedundantPlane.V line 23
  2. def OAI.BoltzmannNonuniqueness.RedundantPlane.normSq line 25
  3. def OAI.BoltzmannNonuniqueness.RedundantPlane.coordinateMatrix line 27
  4. def OAI.BoltzmannNonuniqueness.RedundantPlane.coordinates line 32
  5. theorem OAI.BoltzmannNonuniqueness.RedundantPlane.normSq_pos line 34
  6. theorem OAI.BoltzmannNonuniqueness.RedundantPlane.coordinateMatrix_det line 39
  7. theorem OAI.BoltzmannNonuniqueness.RedundantPlane.coordinates_apply line 47
  8. theorem OAI.BoltzmannNonuniqueness.RedundantPlane.cross_coordinates line 54
  9. theorem OAI.BoltzmannNonuniqueness.RedundantPlane.coordinates_map_volume line 67
  10. def OAI.BoltzmannNonuniqueness.RedundantPlane.normalDensity line 91
  11. theorem OAI.BoltzmannNonuniqueness.RedundantPlane.measurable_normalDensity line 93
  12. theorem OAI.BoltzmannNonuniqueness.RedundantPlane.normalDensity_le_one line 96
  13. theorem OAI.BoltzmannNonuniqueness.RedundantPlane.normalDensity_support line 99
  14. theorem OAI.BoltzmannNonuniqueness.RedundantPlane.lintegral_normalDensity line 103
  15. theorem OAI.BoltzmannNonuniqueness.RedundantPlane.normSq_nonneg line 107
  16. theorem OAI.BoltzmannNonuniqueness.RedundantPlane.cross_normSq_identity line 111
  17. theorem OAI.BoltzmannNonuniqueness.RedundantPlane.coordinates_last line 116
  18. theorem OAI.BoltzmannNonuniqueness.RedundantPlane.normSq_decomposition line 120
  19. theorem OAI.BoltzmannNonuniqueness.RedundantPlane.normSq_parameter_bound line 127
  20. def OAI.BoltzmannNonuniqueness.RedundantPlane.splitThree line 158
  21. theorem OAI.BoltzmannNonuniqueness.RedundantPlane.splitThree_apply line 163
  22. theorem OAI.BoltzmannNonuniqueness.RedundantPlane.splitThree_measurePreserving line 166
  23. theorem OAI.BoltzmannNonuniqueness.RedundantPlane.lintegral_redundant line 170
  24. theorem OAI.BoltzmannNonuniqueness.RedundantPlane.redundant_coordinates_integral line 192