OAI/MathematicalPhysics/Transonic/Shooting/EulerCoordinates.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SepticProfile.SonicShooting.coord line 11

   Source documentation

   Inverse of the source Euler compactification, in the normalized radius.

   def coord (z : ℝ) : ℝ := (1-z)/(501/500-z)

2. def OAI.SepticProfile.SonicShooting.endRadius line 12
3. lemma OAI.SepticProfile.SonicShooting.endRadius_bounds line 14
4. lemma OAI.SepticProfile.SonicShooting.coord_end line 25
5. lemma OAI.SepticProfile.SonicShooting.coord_range line 33
6. lemma OAI.SepticProfile.SonicShooting.coord_ninety_nine line 51
7. lemma OAI.SepticProfile.SonicShooting.coord_derivative line 53
8. lemma OAI.SepticProfile.SonicShooting.coord_field line 60