OAI/Analysis/Conductivity/Variational/NormalStretch.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ScalarConductivity.splitJacobian_det line 27
2. def OAI.ScalarConductivity.normalStretch line 37
3. lemma OAI.ScalarConductivity.normalStretch_det line 40
4. lemma OAI.ScalarConductivity.normalStretch_push line 44
5. lemma OAI.ScalarConductivity.normalStretch_eq_splitJacobian line 57
6. lemma OAI.ScalarConductivity.preliminary_segment line 69
7. theorem OAI.ScalarConductivity.affine_synchronized_path line 104
8. lemma OAI.ScalarConductivity.measure_image_le_det line 130
9. lemma OAI.ScalarConductivity.chart_impure_measure_le line 146