OAI/Geometry/CylinderCovering/Singular/ParameterRange.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CylinderCovering.SingularParameterRange.critical_exponent_bounds line 12
2. lemma OAI.CylinderCovering.SingularParameterRange.numerator_negative_iff line 18
3. theorem OAI.CylinderCovering.SingularParameterRange.coefficient_negative_iff line 31
4. lemma OAI.CylinderCovering.SingularParameterRange.coefficient_at_critical line 48
5. lemma OAI.CylinderCovering.SingularParameterRange.coefficient_at_one line 55
6. theorem OAI.CylinderCovering.SingularParameterRange.coefficient_limit_at_one line 58
7. theorem OAI.CylinderCovering.SingularParameterRange.cutoff_window_nonempty_iff line 65
8. theorem OAI.CylinderCovering.SingularParameterRange.endpoint_derivative_determinant line 80
9. theorem OAI.CylinderCovering.SingularParameterRange.endpoint_derivative_squareZero line 84
10. theorem OAI.CylinderCovering.SingularParameterRange.endpoint_eigenvalue_eq_zero line 91
11. theorem OAI.CylinderCovering.SingularParameterRange.statement line 104