OAI/Probability/LatticeSurface/Dynamics/LogDet.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TangentialJacobian.jacobianCost line 37
2. lemma OAI.TangentialJacobian.jacobianCost_nonneg line 40
3. lemma OAI.TangentialJacobian.trace_sandwich_bound line 45
4. lemma OAI.TangentialJacobian.norm_inverse_one_add_le_two line 66
5. lemma OAI.TangentialJacobian.inverse_line_trace_identity line 83
6. lemma OAI.TangentialJacobian.logdet_line_deriv line 94
7. lemma OAI.TangentialJacobian.logdet_lower_bound line 106