OAI/MathematicalPhysics/Boltzmann/Branching/MediumStateCollision.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

The positive marked collision kernel of a measurable two-beam medium

  1. abbrev OAI.BoltzmannNonuniqueness.ReferenceGeometry.MediumState line 18
  2. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.markedChildKernel line 20
  3. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.markedChildKernel_isMarkov line 28
  4. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumMarkedRate line 33
  5. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumMarkedRate_measurable line 37
  6. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumMarkedKernel line 53
  7. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumMarkedKernel_isSFinite line 56
  8. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumMarkedKernel_apply line 62
  9. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumCollisionKernel line 68
  10. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumCollisionKernel_isSFinite line 71
  11. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumMarkedKernel_lintegral line 76
  12. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumParameterDensity_ne_top line 108
  13. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumEventDensity line 117
  14. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumEventDensity_measurable line 121
  15. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumEventKernel line 125
  16. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumEventKernel_isSFinite line 130
  17. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumEventKernel_lintegral line 141
  18. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumEventKernel_pow_isSFinite line 157
  19. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumCollisionKernel_lintegral line 185
  20. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumCollisionKernel_mass line 194
  21. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumCollisionKernel_projection line 199
  22. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumCollisionKernel_mass_exact line 213
  23. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumCollisionKernel_mass_bound line 229
  24. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.medium_parameter_integral line 256
  25. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumEventKernel_physical_lintegral line 289
  26. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumWord_integral line 340
  27. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumFlightSeed line 375
  28. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.finishMediumFlight_measurable line 378
  29. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumFlightSeed_measurable line 382
  30. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalBlockTarget_measurable line 387
  31. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumBlockMass_kernel line 392
  32. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumEndpointKernel line 422
  33. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumEndpointKernel_isSFinite line 427
  34. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumEndpointKernel_lintegral line 437
  35. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumEndpointKernel_apply line 449
  36. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumBlockMass_endpoints line 459
  37. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumStateCollision line 487
  38. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumStateCollision_sFinite line 493
  39. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumStateCollision_lintegral line 498