OAI/MathematicalPhysics/Transonic/Phase/Timelike.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SepticProfile.minkowskiSquare line 11
2. lemma OAI.SepticProfile.GlobalProfile.radialH_integrand_factor line 15
3. lemma OAI.SepticProfile.GlobalProfile.s0_coordinate_derivative_simple line 25
4. lemma OAI.SepticProfile.sum_coordinate_sq line 38
5. lemma OAI.SepticProfile.GlobalProfile.s0_minkowskiSquare line 44
6. lemma OAI.SepticProfile.GlobalProfile.s0_timelike line 58
7. lemma OAI.SepticProfile.radiusSq_smooth line 63
8. lemma OAI.SepticProfile.GlobalProfile.s0_smooth line 68