OAI/MathematicalPhysics/Boltzmann/Compactness/PhysicalGlobalRenormalized.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Remaining-flight time and characteristic spacetime coordinates

  1. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.flightCharacteristicEquiv line 24
  2. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.flightCharacteristic_advance line 40
  3. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.translated_time_lintegral line 50
  4. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.physical_conserved_test line 74
  5. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.physical_mass_conservation line 98
  6. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.physical_momentum_coordinate line 109
  7. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.physical_momentum_conservation line 121
  8. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.physical_energy_le line 152
  9. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.velocityPhaseBall line 201
  10. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.velocityPhaseBall_measurable line 203
  11. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalGainEndpoint_velocity_ball line 206
  12. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.velocityPhaseBall_subset_entry line 215
  13. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.physical_entry_eventually_lateBox line 228
  14. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.geometric_density_lateBox_access line 246
  15. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.physical_renormalized_integrable line 275
  16. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.physical_renormalized_balance_terminal_zero line 289
  17. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.flightCharacteristic_waiting_lintegral line 318
  18. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.flightCharacteristic_waiting_map line 342
  19. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.physical_eq_density_nonnegative line 364
  20. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.physical_global_mass line 382
  21. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.physical_global_renormalized line 412