OAI/Analysis/Conductivity/Sources/AngularGraph.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ScalarConductivity.smoothAxisModeJet_ae line 18
  2. lemma OAI.ScalarConductivity.sourceAngularLpJet_coefficient line 32
  3. theorem OAI.ScalarConductivity.sourceAngularLpJet_graph line 54
  4. lemma OAI.ScalarConductivity.hasDerivAt_outer_of_strict_comp line 81
  5. lemma OAI.ScalarConductivity.hasStrictDerivAt_faceRayAngle line 92
  6. lemma OAI.ScalarConductivity.faceRayDensity_pos' line 98
  7. lemma OAI.ScalarConductivity.torusDirectionalDerivative_of_face line 102
  8. lemma OAI.ScalarConductivity.hasDerivAt_coordinate_update line 113
  9. lemma OAI.ScalarConductivity.physicalTestCovector_update line 123
  10. lemma OAI.ScalarConductivity.sourceAngularTest_face0 line 130
  11. lemma OAI.ScalarConductivity.sourceAngularTest_face1 line 160
  12. lemma OAI.ScalarConductivity.sourceAngularAxial_face line 190
  13. theorem OAI.ScalarConductivity.sourceAngularJet_face line 214