OAI/Probability/LatticeSurface/Dynamics/ShiftAnalysis.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TangentialJacobian.opNorm_le_of_row_sum line 24
2. lemma OAI.FeasibleShift.freeShift_derivative_row line 50
3. lemma OAI.FeasibleShift.freeShift_derivative_column line 85
4. lemma OAI.FeasibleShift.freeShift_derivative_cost line 107
5. lemma OAI.FeasibleShift.freeShift_derivative_opNorm line 138
6. lemma OAI.FeasibleShift.freeShift_det_identity line 162
7. lemma OAI.FeasibleShift.freeShift_divergence_identities line 194
8. lemma OAI.TangentialJacobian.continuous_trace line 229
9. lemma OAI.TangentialJacobian.continuous_jacobianCost line 233
10. lemma OAI.TangentialJacobian.uniform_image_area line 245
11. lemma OAI.TangentialJacobian.jacobian_integrable line 264
12. lemma OAI.TangentialJacobian.uniform_image_lower_bound line 270
13. lemma OAI.TangentialJacobian.markov_real line 297
14. lemma OAI.TangentialJacobian.event_volume_of_moments line 306