OAI/Analysis/Conductivity/Fourier/AttachedEndPoisson.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ScalarConductivity.endAxialAffine line 11
  2. def OAI.ScalarConductivity.endAxialMatrix line 14
  3. lemma OAI.ScalarConductivity.endAxialAffine_contDiff line 16
  4. lemma OAI.ScalarConductivity.endAxialAffine_hasFDeriv line 27
  5. lemma OAI.ScalarConductivity.torusAngles_endAxialAffine line 44
  6. def OAI.ScalarConductivity.attachedEndPoissonField line 49
  7. lemma OAI.ScalarConductivity.measurable_attachedEndPoissonField line 53
  8. lemma OAI.ScalarConductivity.attachedEndPoissonField_angular line 60
  9. lemma OAI.ScalarConductivity.attachedEndPoissonField_piece line 67
  10. lemma OAI.ScalarConductivity.attachedEndPoissonField_local_eq line 77
  11. theorem OAI.ScalarConductivity.attachedEndPoissonField_hasFDeriv line 90
  12. lemma OAI.ScalarConductivity.attachedEndPoissonField_eq_continuation line 118
  13. theorem OAI.ScalarConductivity.attachedEndPoissonField_localLip line 135