OAI/Geometry/IsometricImmersion/Caps/EllipticRatio.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SmoothLocal.Weighted.ellipticRatioConstant line 14
2. theorem OAI.SmoothLocal.Weighted.ellipticRatioConstant_nonneg line 18
3. theorem OAI.SmoothLocal.Weighted.square_bound_of_abs_bound line 24
4. theorem OAI.SmoothLocal.Weighted.elliptic_ratio_scalar line 30
5. theorem OAI.SmoothLocal.Weighted.actual_elliptic_ratio line 117
6. def OAI.SmoothLocal.Weighted.ellipticCutoffDerivativeConstant line 131
7. theorem OAI.SmoothLocal.Weighted.ellipticCutoffDerivativeConstant_nonneg line 134
8. theorem OAI.SmoothLocal.Weighted.ellipticWeight_partial_bound_common line 141
9. theorem OAI.SmoothLocal.Weighted.ellipticCutoff_actual_ratio line 170