OAI/Analysis/Conductivity/Branching/ChildCoordinateAnalysis.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ScalarConductivity.sourceChildHomeomorph line 11
2. def OAI.ScalarConductivity.sourceChildJacobian line 19
3. def OAI.ScalarConductivity.sourceChildDerivative line 22
4. lemma OAI.ScalarConductivity.sourceChildDerivative_apply line 25
5. lemma OAI.ScalarConductivity.sourceChildCoordinates_contDiff line 30
6. lemma OAI.ScalarConductivity.sourceChildCoordinates_hasFDeriv line 34
7. lemma OAI.ScalarConductivity.sourceChildDerivative_det line 41
8. lemma OAI.ScalarConductivity.sourceChildDerivative_norm line 47
9. lemma OAI.ScalarConductivity.sourceChild_energy line 60
10. lemma OAI.ScalarConductivity.integral_sourceChild_preimage line 71