OAI/MathematicalPhysics/Boltzmann/Branching/CharacteristicCoordinates.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Almost-everywhere velocity-fiber bounds along almost every free path

  1. theorem OAI.BoltzmannNonuniqueness.measurableSet_ae_velocity_bound line 16
  2. theorem OAI.BoltzmannNonuniqueness.ae_velocity_bound_along_paths line 31
  3. def OAI.BoltzmannNonuniqueness.EuclideanFlight.characteristicEquiv line 72
  4. theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.characteristic_measurePreserving line 89
  5. theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.integral_eq_zero_of_characteristics line 103