OAI/MathematicalPhysics/Boltzmann/Jets/JetBarrierKinetic.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

The exact axial thermal-coordinate map for a free core

  1. def OAI.BoltzmannNonuniqueness.JetCoreMap.axialMap line 17
  2. def OAI.BoltzmannNonuniqueness.JetCoreMap.axialInverse line 20
  3. def OAI.BoltzmannNonuniqueness.JetCoreMap.sourceFoot line 23
  4. theorem OAI.BoltzmannNonuniqueness.JetCoreMap.sourceFoot_eq line 26
  5. theorem OAI.BoltzmannNonuniqueness.JetCoreMap.axialMap_spec line 31
  6. theorem OAI.BoltzmannNonuniqueness.JetCoreMap.inverse_map line 40
  7. theorem OAI.BoltzmannNonuniqueness.JetCoreMap.map_inverse line 47
  8. theorem OAI.BoltzmannNonuniqueness.JetCoreMap.axialMap_derivative line 62
  9. def OAI.BoltzmannNonuniqueness.JetCoreMap.axialHomeomorph line 85
  10. def OAI.BoltzmannNonuniqueness.JetCoreJacobian.jacobian line 116
  11. theorem OAI.BoltzmannNonuniqueness.JetCoreJacobian.jacobian_pos line 119
  12. theorem OAI.BoltzmannNonuniqueness.JetCoreJacobian.integral_substitution line 125
  13. theorem OAI.BoltzmannNonuniqueness.JetCoreJacobian.integrable_substitution line 137
  14. theorem OAI.BoltzmannNonuniqueness.JetCoreJacobian.compression_bound line 149
  15. def OAI.BoltzmannNonuniqueness.JetBarrierKinetic.compression line 188
  16. def OAI.BoltzmannNonuniqueness.JetBarrierKinetic.squaredError line 191
  17. theorem OAI.BoltzmannNonuniqueness.JetBarrierKinetic.compression_nonneg line 194
  18. theorem OAI.BoltzmannNonuniqueness.JetBarrierKinetic.squaredError_derivative line 201
  19. theorem OAI.BoltzmannNonuniqueness.JetBarrierKinetic.kineticExponent_derivative line 216
  20. theorem OAI.BoltzmannNonuniqueness.JetBarrierKinetic.kineticExponent_derivative_lower line 230