OAI/Analysis/Conductivity/Flux/PhysicalTensorPatch.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ScalarConductivity.sourceFlatPatch line 15
  2. lemma OAI.ScalarConductivity.isCompact_sourceFlatPatch line 18
  3. lemma OAI.ScalarConductivity.continuousAt_sourceCollarInverse_patch line 21
  4. lemma OAI.ScalarConductivity.continuousOn_attachedPhysicalFlatTensor line 54
  5. def OAI.ScalarConductivity.attachedPatchTensor line 61
  6. lemma OAI.ScalarConductivity.measurable_attachedPatchTensor line 65
  7. lemma OAI.ScalarConductivity.attachedPatchTensor_symmetric line 71
  8. def OAI.ScalarConductivity.attachedFaceTensorList line 92
  9. lemma OAI.ScalarConductivity.attachedFaceTensorList_cons line 98
  10. lemma OAI.ScalarConductivity.attachedFaceTensorList_measurable line 106
  11. lemma OAI.ScalarConductivity.attachedFaceTensorList_symmetric line 115
  12. lemma OAI.ScalarConductivity.identity_matrix_energy_bounds line 127
  13. lemma OAI.ScalarConductivity.attachedFaceTensorList_elliptic line 139
  14. lemma OAI.ScalarConductivity.attachedFaceTensorList_outside line 167
  15. lemma OAI.ScalarConductivity.attachedFaceTensorList_local line 177
  16. def OAI.ScalarConductivity.attachedCollarTensor line 195
  17. theorem OAI.ScalarConductivity.attachedCollarTensor_properties line 199