OAI/Analysis/Conductivity/Flux/PhysicalBlockTensor.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ScalarConductivity.childAxis_pi_norm line 17
  2. lemma OAI.ScalarConductivity.sourceChildTensorPush_measurable line 27
  3. lemma OAI.ScalarConductivity.sourceChildTensorPush_norm_bound line 42
  4. def OAI.ScalarConductivity.physicalEndTensor line 56
  5. lemma OAI.ScalarConductivity.physicalEndTensor_properties line 61
  6. def OAI.ScalarConductivity.physicalBlockTensorList line 94
  7. lemma OAI.ScalarConductivity.physicalBlockTensorList_cons line 99
  8. lemma OAI.ScalarConductivity.physicalBlockTensorList_properties line 104
  9. def OAI.ScalarConductivity.physicalBlockTensor line 151
  10. lemma OAI.ScalarConductivity.physicalBlockTensor_local_list line 155
  11. lemma OAI.ScalarConductivity.physicalBlockTensor_local line 170
  12. lemma OAI.ScalarConductivity.physicalBlockTensorList_outside line 175
  13. theorem OAI.ScalarConductivity.physicalBlockTensor_properties line 185