OAI/MathematicalPhysics/Transonic/Phase/Coordinates.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SepticProfile.PhysicalSpace line 11
2. def OAI.SepticProfile.radiusSq line 12
3. def OAI.SepticProfile.radius line 13
4. def OAI.SepticProfile.coordinateLine line 14
5. lemma OAI.SepticProfile.radiusSq_nonneg line 16
6. lemma OAI.SepticProfile.radius_sq line 18
7. lemma OAI.SepticProfile.coordinateLine_zero line 20
8. lemma OAI.SepticProfile.radiusSq_coordinateLine line 23
9. lemma OAI.SepticProfile.radiusSq_coordinate_derivative line 33
10. lemma OAI.SepticProfile.GlobalProfile.radialH_derivative line 41
11. def OAI.SepticProfile.GlobalProfile.s0 line 48
12. lemma OAI.SepticProfile.GlobalProfile.s0_radial line 50
13. lemma OAI.SepticProfile.GlobalProfile.s0_coordinate_derivative line 54
14. lemma OAI.SepticProfile.GlobalProfile.s0_time_derivative line 73