OAI/Analysis/Conductivity/Geometry/RectanglePoincare.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ScalarConductivity.RectFootprint.prism_volume line 11
  2. lemma OAI.ScalarConductivity.RectFootprint.prism_volume_pos line 17
  3. lemma OAI.ScalarConductivity.RectFootprint.prism_real_pos line 23
  4. def OAI.ScalarConductivity.RectFootprint.poincareConstant line 29
  5. def OAI.ScalarConductivity.RectFootprint.average line 32
  6. lemma OAI.ScalarConductivity.RectFootprint.poincareConstant_nonneg line 35
  7. theorem OAI.ScalarConductivity.RectFootprint.poincare line 38
  8. lemma OAI.ScalarConductivity.rectangle_energy_mono line 49
  9. theorem OAI.ScalarConductivity.RectFootprint.poincare_in line 56
  10. def OAI.ScalarConductivity.patchCluster line 68
  11. lemma OAI.ScalarConductivity.patchCluster_mono line 73
  12. lemma OAI.ScalarConductivity.subset_patchCluster line 80
  13. def OAI.ScalarConductivity.patchPoincareConstant line 85
  14. lemma OAI.ScalarConductivity.patchPoincareConstant_nonneg line 91
  15. theorem OAI.ScalarConductivity.connected_patch_poincare line 102