OAI/Analysis/Conductivity/Flux/CentralCylinderGreen.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ScalarConductivity.central_cylinder_green line 12
  2. theorem OAI.ScalarConductivity.central_attached_weak_solution_exists line 36
  3. def OAI.ScalarConductivity.flatCylinderMatrix line 73
  4. lemma OAI.ScalarConductivity.flatCylinderMatrix_symmetric line 76
  5. lemma OAI.ScalarConductivity.flatCylinderMatrix_energy line 81
  6. lemma OAI.ScalarConductivity.flatCylinderMatrix_coercive line 87
  7. lemma OAI.ScalarConductivity.sourceFaceAngleMatrix_det line 96
  8. lemma OAI.ScalarConductivity.sourceFaceAngleMatrix_det_pos line 103
  9. lemma OAI.ScalarConductivity.sourceCartesianGradientMatrix_det_ne_zero line 114
  10. def OAI.ScalarConductivity.sourceFlatDensity line 122
  11. lemma OAI.ScalarConductivity.sourceFlatDensity_pos line 125
  12. def OAI.ScalarConductivity.sourceFlatTensor line 131
  13. lemma OAI.ScalarConductivity.sourceFlatTensor_symmetric line 137
  14. lemma OAI.ScalarConductivity.inverse_congruence_energy line 142
  15. theorem OAI.ScalarConductivity.sourceFlatTensor_energy line 153
  16. theorem OAI.ScalarConductivity.sourceFlatTensor_energy_density line 160