OAI/MathematicalPhysics/Boltzmann/Branching/ScaledBoundedEvent.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Equal scaled partner measures give equal scaled normal-angle gains

  1. theorem OAI.BoltzmannNonuniqueness.normalGainKernel_smul_eq_of_measure_smul_eq line 23
  2. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.scaled_time_lintegral line 55
  3. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.flightScaleEquiv line 93
  4. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.flightScale_advance line 116
  5. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.normalized_mediumPoint line 128
  6. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.scaled_waiting_lintegral line 159
  7. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.scaled_waiting_map line 186
  8. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumCollisionKernel_normalized line 214
  9. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.normalized_flight_location line 221
  10. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumStateCollision_scale_map line 229
  11. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.densityScaledCollision line 261
  12. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.densityScaledCollision_sFinite line 265
  13. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.densityScaledCollision_lintegral line 271
  14. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.densityScaledEventKernel line 278
  15. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.densityScaledEventKernel_sFinite line 282
  16. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.densityScaledEvent_scale_map line 287
  17. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.boundedDensityScaledEvent line 324
  18. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.boundedDensityScaledEvent_sFinite line 328
  19. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.boundedPhysicalEvent line 333
  20. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.boundedPhysicalEvent_sFinite line 338
  21. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.boundedDensityScaledEvent_map line 343
  22. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.boundedDensityScaledEvent_pow_map line 355