OAI/Geometry/Relativity/CKS/InducedSphereCalculus.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CKSInducedSphere.U line 15
  2. lemma OAI.CKSInducedSphere.U_open line 16
  3. lemma OAI.CKSInducedSphere.e_apply line 20
  4. lemma OAI.CKSInducedSphere.expand_vec line 23
  5. def OAI.CKSInducedSphere.grad line 27
  6. def OAI.CKSInducedSphere.hess line 29
  7. def OAI.CKSInducedSphere.third line 31
  8. lemma OAI.CKSInducedSphere.partial_smooth line 33
  9. lemma OAI.CKSInducedSphere.hess_smooth line 37
  10. lemma OAI.CKSInducedSphere.partial_of_clm line 41
  11. lemma OAI.CKSInducedSphere.partial_partial line 44
  12. lemma OAI.CKSInducedSphere.partial_comm line 53
  13. lemma OAI.CKSInducedSphere.third_cycle line 59
  14. lemma OAI.CKSInducedSphere.fderiv_expand line 69
  15. lemma OAI.CKSInducedSphere.smooth_diff line 73
  16. lemma OAI.CKSInducedSphere.pd_add line 76
  17. lemma OAI.CKSInducedSphere.pd_sub line 81
  18. lemma OAI.CKSInducedSphere.pd_mul line 86
  19. lemma OAI.CKSInducedSphere.pd_sum line 93
  20. lemma OAI.CKSInducedSphere.pd_const line 98
  21. lemma OAI.CKSInducedSphere.pd_const_mul line 101
  22. lemma OAI.CKSInducedSphere.pd_div_const line 105
  23. lemma OAI.CKSInducedSphere.coordinate_smooth line 110
  24. lemma OAI.CKSInducedSphere.pd_coordinate line 113
  25. lemma OAI.CKSInducedSphere.proj_smooth line 119
  26. lemma OAI.CKSInducedSphere.pd_proj line 122
  27. lemma OAI.CKSInducedSphere.trace_smooth line 131
  28. lemma OAI.CKSInducedSphere.pd_tangentTrace line 137
  29. def OAI.CKSInducedSphere.roundLaplacian line 151
  30. def OAI.CKSInducedSphere.traceFreeHess line 153
  31. def OAI.CKSInducedSphere.tensorDivergence line 155
  32. def OAI.CKSInducedSphere.sphereGradient line 159
  33. lemma OAI.CKSInducedSphere.roundLaplacian_smooth line 162
  34. lemma OAI.CKSInducedSphere.pd_roundLaplacian line 167
  35. lemma OAI.CKSInducedSphere.traceFreeHess_smooth line 182
  36. lemma OAI.CKSInducedSphere.pd_traceFreeHess line 189
  37. lemma OAI.CKSInducedSphere.unit_sum_sq line 218
  38. theorem OAI.CKSInducedSphere.divergence_traceFreeHess line 222