OAI/MathematicalPhysics/Boltzmann/Branching/CharacteristicPhysicalGain.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

A common physical cylinder for all time tests of a fixed compact phase test

  1. theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.exists_timePhase_cylinder line 19
  2. theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.exists_timePhase_cylinder_for_support line 75
  3. theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.coldCylinderSet_mono_radius line 132
  4. theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.exists_phase_cylinder line 137
  5. theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.exists_timePhase_cylinder_cover line 152
  6. theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.cylinder_phase_integral_eq line 169
  7. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.physicalCharacteristicGain line 196
  8. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.physicalCharacteristicGain_measurable line 199
  9. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.physicalCharacteristicGain_nonneg line 204
  10. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.characteristic_clipped_gain_tendsto line 208