OAI/Analysis/Conductivity/Sources/AngularTrace.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ScalarConductivity.rectangularRay_abs line 13
  2. lemma OAI.ScalarConductivity.rectangularRay_coordinate_bound line 21
  3. def OAI.ScalarConductivity.sourceRayCoordinates line 31
  4. def OAI.ScalarConductivity.sourceRayBox line 35
  5. lemma OAI.ScalarConductivity.sourceRayCoordinates_mem line 37
  6. lemma OAI.ScalarConductivity.continuous_sourceRayCoordinates line 48
  7. def OAI.ScalarConductivity.sourceRayConstant line 60
  8. lemma OAI.ScalarConductivity.sourceRayConstant_nonneg line 62
  9. lemma OAI.ScalarConductivity.sourceRayCoordinates_difference line 67
  10. def OAI.ScalarConductivity.sourceAngularPolynomial line 91
  11. def OAI.ScalarConductivity.sourceAngularCollar line 95
  12. lemma OAI.ScalarConductivity.contDiff_sourceAngularPolynomial line 98
  13. lemma OAI.ScalarConductivity.continuous_sourceAngularCollar line 104
  14. theorem OAI.ScalarConductivity.sourceAngularTrace_summable line 107