OAI/MathematicalPhysics/Boltzmann/Branching/HotPositiveRegion.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

A compact kinetic cutoff confines its velocity average to a compact base

  1. theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.average_eq_zero_outside_projection line 20
  2. theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.average_difference_norm_restrict line 30
  3. def OAI.BoltzmannNonuniqueness.EuclideanFlight.hotCharacteristicEquiv line 62
  4. theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.hotCharacteristic_measurePreserving line 65
  5. def OAI.BoltzmannNonuniqueness.EuclideanFlight.cylinderPullback line 69
  6. theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.cylinderPullback_integrable line 73
  7. theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.cylinderPullback_integral line 82
  8. def OAI.BoltzmannNonuniqueness.EuclideanFlight.sourcePullback line 98
  9. instance OAI.BoltzmannNonuniqueness.EuclideanFlight.sourcePullback_finite line 101
  10. theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.sourcePullback_integral line 106
  11. def OAI.BoltzmannNonuniqueness.Published.DunfordPettis1940HotPairWindows line 136
  12. def OAI.BoltzmannNonuniqueness.EuclideanFlight.hotRegion line 157
  13. theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.hotRegion_open line 160
  14. theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.hotRegion_nonempty line 164
  15. theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.hotBaseSet_closed line 168
  16. theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.hotRegion_ae line 171