OAI/Analysis/Conductivity/Fourier/RectangularTorusAtlas.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ScalarConductivity.squareFaceBase line 11
  2. def OAI.ScalarConductivity.squareFaceDirection line 12
  3. def OAI.ScalarConductivity.squareFace line 13
  4. def OAI.ScalarConductivity.squareFaceParameter line 15
  5. lemma OAI.ScalarConductivity.squareFace_parameter line 18
  6. lemma OAI.ScalarConductivity.squareFace_max line 22
  7. lemma OAI.ScalarConductivity.squareFace_determinant line 27
  8. lemma OAI.ScalarConductivity.squareFace_min_max line 32
  9. def OAI.ScalarConductivity.sourceRadialCenter line 54
  10. def OAI.ScalarConductivity.sourceRadialWidth line 55
  11. def OAI.ScalarConductivity.sourceCollarRadius line 57
  12. def OAI.ScalarConductivity.sourceCollarPiece line 60
  13. def OAI.ScalarConductivity.sourceRadial line 65
  14. def OAI.ScalarConductivity.sourceCrossCoordinates line 67
  15. def OAI.ScalarConductivity.sourceCollarTime line 70
  16. lemma OAI.ScalarConductivity.sourceCollarRadius_bounds line 73
  17. lemma OAI.ScalarConductivity.sourceCollarPiece_radial line 85
  18. lemma OAI.ScalarConductivity.sourceCollarPiece_cross line 100
  19. lemma OAI.ScalarConductivity.sourceCollarPiece_time line 112
  20. def OAI.ScalarConductivity.sourceCollarJacobian line 120
  21. def OAI.ScalarConductivity.sourceCollarDerivative line 129
  22. lemma OAI.ScalarConductivity.squareFace_coord_hasFDeriv line 133
  23. lemma OAI.ScalarConductivity.sourceCollarPiece_hasFDeriv line 139
  24. lemma OAI.ScalarConductivity.sourceCollarPiece_contDiff line 170
  25. lemma OAI.ScalarConductivity.sourceCollarJacobian_det line 176
  26. lemma OAI.ScalarConductivity.sourceCollarJacobian_det_ne_zero line 189