OAI/Analysis/Conductivity/Sobolev/CollarLpPullback.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ScalarConductivity.sourceCylinderMeasure line 12
2. lemma OAI.ScalarConductivity.sourceCylinderMeasure_eq line 16
3. def OAI.ScalarConductivity.sourcePhysicalCoordinates line 24
4. lemma OAI.ScalarConductivity.measurable_sourcePhysicalCoordinates line 27
5. lemma OAI.ScalarConductivity.sourcePhysicalCoordinates_angular line 33
6. lemma OAI.ScalarConductivity.sourcePhysicalCoordinates_measurePreserving line 38
7. def OAI.ScalarConductivity.sourceCollarPullback line 53
8. lemma OAI.ScalarConductivity.sourceCollarPullback_ae line 61
9. lemma OAI.ScalarConductivity.sourceCollarPullback_ae_of_ae line 73
10. lemma OAI.ScalarConductivity.sourceCollarPullback_hasSum line 82