OAI/MathematicalPhysics/Boltzmann/Branching/DampedBoundedEndpointTransport.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

The measurable two-beam collision law under local density normalization

  1. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedMediumCollision_normalized line 28
  2. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedMediumStateCollision_scale_map line 34
  3. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.uniform_damped_lateBox_geometric_block line 67
  4. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedCharacteristicKernel line 112
  5. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedCharacteristicKernel_sFinite line 116
  6. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedStateCollision_eq_transport line 121
  7. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedEventKernel_pow_characteristic line 126
  8. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedCharacteristicKernel_lintegral line 137
  9. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.characteristicBeamFrequency line 167
  10. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.characteristicBeamFrequency_measurable line 172
  11. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedCharacteristicKernel_projection line 182
  12. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedDensityScaledCollision line 224
  13. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedDensityScaledCollision_sFinite line 228
  14. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedDensityScaledCollision_lintegral line 234
  15. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedDensityScaledEventKernel line 241
  16. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedDensityScaledEventKernel_sFinite line 245
  17. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedDensityScaledEvent_scale_map line 250
  18. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedBoundedDensityScaledEvent line 287
  19. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedBoundedDensityScaledEvent_sFinite line 291
  20. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedBoundedDensityScaledEvent_map line 296
  21. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedBoundedDensityScaledEvent_pow_map line 308
  22. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.characteristicVelocityBox line 334
  23. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.characteristicVelocityBox_measurable line 336
  24. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedBoundedCharacteristicKernel line 340
  25. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedBoundedCharacteristicKernel_sFinite line 344
  26. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedBoundedPhysicalEvent_transport line 349
  27. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedBoundedPhysicalEvent_pow_transport line 362
  28. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.densityScaledCharacteristicKernel line 385
  29. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.densityScaledCharacteristicKernel_sFinite line 389
  30. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.boundedDensityScaledCharacteristicKernel line 393
  31. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.boundedDensityScaledCharacteristicKernel_sFinite line 397
  32. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedDensityScaledCollision_transport line 403
  33. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedBoundedDensityScaledEvent_transport line 410
  34. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedBoundedDensityScaledEvent_pow_transport line 424
  35. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.densityScaledCharacteristicKernel_projection line 448
  36. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedDensityScaled_endpoint_characteristic line 489
  37. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedBoundedEndpoint_characteristic line 528