OAI/Probability/LatticeSurface/Dynamics/JacobianIdentity.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TangentialJacobian.lipschitz_image_null line 13
2. lemma OAI.TangentialJacobian.lipschitz_area line 20
3. lemma OAI.TangentialJacobian.det_one_add_ne_zero line 41
4. lemma OAI.TangentialJacobian.det_one_add_pos line 48
5. lemma OAI.TangentialJacobian.lipschitz_id_add_smul line 63
6. lemma OAI.TangentialJacobian.det_fderiv_positive line 78
7. lemma OAI.TangentialJacobian.ae_fderiv_id_add_smul line 85
8. lemma OAI.TangentialJacobian.det_lintegral_of_invariant line 92
9. lemma OAI.TangentialJacobian.det_jacobian_measurable line 105
10. lemma OAI.TangentialJacobian.det_integral_of_invariant line 110