OAI/MathematicalPhysics/Boltzmann/Branching/CharacteristicProductTest.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Smooth compact tests in free-characteristic coordinates

  1. abbrev OAI.BoltzmannNonuniqueness.EuclideanFlight.CharacteristicPhase line 17
  2. theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.characteristicEquiv_contDiff line 19
  3. theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.characteristicEquiv_symm_contDiff line 24
  4. def OAI.BoltzmannNonuniqueness.EuclideanFlight.characteristicHomeomorph line 30
  5. def OAI.BoltzmannNonuniqueness.EuclideanFlight.testPullback line 35
  6. theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.testPullback_contDiff line 38
  7. theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.testPullback_compact line 42
  8. def OAI.BoltzmannNonuniqueness.EuclideanFlight.timeDerivative line 46
  9. theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.timeDerivative_continuous line 49
  10. theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.testPullback_along line 53
  11. theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.transportDerivative_testPullback line 58
  12. def OAI.BoltzmannNonuniqueness.EuclideanFlight.timePhaseTest line 90
  13. theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.timePhaseTest_contDiff line 93
  14. theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.timePhaseTest_support line 98
  15. theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.timePhaseTest_compact line 106
  16. theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.timeDerivative_timePhaseTest line 112