OAI/MathematicalPhysics/Boltzmann/Jets/BeamNormalOutgoing.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Space-time coordinates normalized by the local cold density

  1. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.normalizedPoint line 20
  2. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.normalizedPoint_measurable line 23
  3. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.BeamCoefficients.normalized line 28
  4. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.normalizedPoint_bounds line 38
  5. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.normalized_beam_near line 52
  6. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.characteristicBeamPoint line 77
  7. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.characteristicBeamJump line 80
  8. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.beamCharacteristicKernel_lintegral line 83
  9. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.beamCharacteristicKernel_independent line 112
  10. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.medium_frequency_seven line 134
  11. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.BeamNear.frequency_margin line 155
  12. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.frequency_le_near_clock_seven line 180
  13. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.beamPartnerKernel line 211
  14. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.beamPartnerKernel_sFinite line 217
  15. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.beamPartnerKernel_apply line 227
  16. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.beamNormalCharacteristicKernel line 255
  17. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.beamNormalCharacteristicKernel_sFinite line 259
  18. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.beamNormalCharacteristicKernel_lintegral line 264
  19. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.normalGain_beam_projection line 290