OAI/MathematicalPhysics/Boltzmann/Branching/BoundedGeometricBlock.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

The finite-speed cone of the velocity-truncated physical histories

  1. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.boundedFlightCone line 23
  2. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.boundedFlightCone_measurable line 26
  3. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.boundedFlightCone_refl line 36
  4. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.boundedFlightCone_trans line 40
  5. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.boundedFlightCone_step line 49
  6. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedDensityScaledEvent_ae_geometry line 74
  7. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedBoundedDensityScaledEvent_ae_cone line 101
  8. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedBoundedDensityScaledEvent_pow_ae_cone line 110
  9. def OAI.BoltzmannNonuniqueness.seedPortion line 143
  10. theorem OAI.BoltzmannNonuniqueness.seedPortion_measurable line 146
  11. theorem OAI.BoltzmannNonuniqueness.seedPortion_iUnion line 150
  12. theorem OAI.BoltzmannNonuniqueness.exists_positive_seedPortion line 169
  13. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.uniform_bounded_local_beam_block line 204
  14. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.uniform_bounded_physical_beam_block line 229
  15. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.boundedMediumEventKernel_eq_physical line 264
  16. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.boundedMediumEventKernel_remaining_le line 270
  17. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.boundedMediumEventKernel_pow_eq_physical line 276
  18. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.densityScaled_bounded_history_map line 294
  19. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedBoundedDensityScaledEvent_localization line 320
  20. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.geometric_bounded_block_growth line 361