OAI/Analysis/Conductivity/Fourier/AngularNormalTrace.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ScalarConductivity.sourceAngularVelocity line 13
  2. lemma OAI.ScalarConductivity.sourceAngular_affine line 17
  3. lemma OAI.ScalarConductivity.sourceAngularVelocity_norm line 22
  4. lemma OAI.ScalarConductivity.continuous_sourceAngularVelocity line 35
  5. lemma OAI.ScalarConductivity.sourceAngular_normal_deriv line 45
  6. theorem OAI.ScalarConductivity.sourceAngular_pointwise_trace line 54
  7. lemma OAI.ScalarConductivity.rayDirection_coe_angle line 82
  8. lemma OAI.ScalarConductivity.rectangularRay_of_direction line 95
  9. def OAI.ScalarConductivity.faceRayAngle line 111
  10. lemma OAI.ScalarConductivity.faceRayAngle_image line 115
  11. lemma OAI.ScalarConductivity.faceRayAngle_endpoints line 147
  12. def OAI.ScalarConductivity.faceRayDensity line 158
  13. lemma OAI.ScalarConductivity.hasDerivAt_faceRayAngle line 162
  14. lemma OAI.ScalarConductivity.continuous_faceRayDensity line 175
  15. lemma OAI.ScalarConductivity.faceRayDensity_bounds line 188