OAI/MathematicalPhysics/Boltzmann/Jets/BeamNormalCharacteristicIdentity.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A density-scaled normal-angle beam source with its exact loss complement

  1. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.scaledBeamNormalKernel line 18
  2. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.scaledBeamNormalKernel_sFinite line 22
  3. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.scaledBeamNormalKernel_apply line 26
  4. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.beamNormalRetainedKernel line 30
  5. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.beamNormalRetainedKernel_sFinite line 35
  6. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.beamNormalRetainedKernel_lintegral line 40
  7. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.beamNormalCharacteristicKernel_eq line 67
  8. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.beamNormalRetainedKernel_eq_scaled line 89