OAI/Analysis/Conductivity/Walls/WallHalfspaceIntegral.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ScalarConductivity.hasCompactSupport_prodMkLeft line 12
  2. lemma OAI.ScalarConductivity.hasCompactSupport_prodMkRight line 22
  3. lemma OAI.ScalarConductivity.wallDerivative_slice line 32
  4. lemma OAI.ScalarConductivity.wallAlong_slice line 38
  5. lemma OAI.ScalarConductivity.wallAlong_integral_slice line 47
  6. theorem OAI.ScalarConductivity.wall_halfspace_flux line 61
  7. lemma OAI.ScalarConductivity.wallAlong_sCoordinate line 95
  8. lemma OAI.ScalarConductivity.wallDerivative_sCoordinate line 98
  9. lemma OAI.ScalarConductivity.wallAlong_sub_box line 101
  10. lemma OAI.ScalarConductivity.wallAlong_neg line 106
  11. lemma OAI.ScalarConductivity.wall_torque_divergence line 110
  12. theorem OAI.ScalarConductivity.wall_matrix_halfspace_moments line 133