OAI/Analysis/Conductivity/Sobolev/ParentFullEndH1.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ScalarConductivity.parentFullEnd_H10 line 14
2. lemma OAI.ScalarConductivity.sourceCollarTime_local_inverse line 73
3. lemma OAI.ScalarConductivity.sourceCollarTime_differentiable_open line 83
4. lemma OAI.ScalarConductivity.attachedCartesianMatrix_axial_derivative line 90
5. def OAI.ScalarConductivity.fullEndFlatCovector line 120
6. lemma OAI.ScalarConductivity.fullAttachedEnd_covector line 124
7. lemma OAI.ScalarConductivity.fullAttachedEndGradient_transport line 141
8. theorem OAI.ScalarConductivity.fullAttachedEnd_test_energy line 161
9. theorem OAI.ScalarConductivity.fullAttachedEnd_test_integral line 178