OAI/Geometry/Relativity/CKS/InducedSphereAlgebra.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CKSInducedSphere.Vec line 10
  2. abbrev OAI.CKSInducedSphere.Mat line 11
  3. def OAI.CKSInducedSphere.proj line 13
  4. def OAI.CKSInducedSphere.dproj line 15
  5. def OAI.CKSInducedSphere.tangentTrace line 18
  6. def OAI.CKSInducedSphere.hessTF line 20
  7. def OAI.CKSInducedSphere.dTangentTrace line 23
  8. def OAI.CKSInducedSphere.dHessTF line 26
  9. def OAI.CKSInducedSphere.divHessTF line 31
  10. def OAI.CKSInducedSphere.roundLap line 34
  11. def OAI.CKSInducedSphere.dRoundLap line 37
  12. lemma OAI.CKSInducedSphere.proj_symm line 40
  13. lemma OAI.CKSInducedSphere.proj_normal line 43
  14. lemma OAI.CKSInducedSphere.proj_idempotent line 51
  15. lemma OAI.CKSInducedSphere.proj_trace line 62
  16. lemma OAI.CKSInducedSphere.projected_dproj line 67
  17. lemma OAI.CKSInducedSphere.contracted_dproj line 78
  18. lemma OAI.CKSInducedSphere.sum3_rotate line 90
  19. lemma OAI.CKSInducedSphere.sum4_comm line 96
  20. lemma OAI.CKSInducedSphere.contraction_left_dproj line 102
  21. lemma OAI.CKSInducedSphere.contraction_left_proj line 113
  22. lemma OAI.CKSInducedSphere.contraction_trace_term line 126
  23. lemma OAI.CKSInducedSphere.contraction_right_dproj line 133
  24. lemma OAI.CKSInducedSphere.sum3_last line 147
  25. def OAI.CKSInducedSphere.normalH line 153
  26. def OAI.CKSInducedSphere.projectedK line 154
  27. def OAI.CKSInducedSphere.projectedTraceDeriv line 156
  28. def OAI.CKSInducedSphere.rawContract line 159
  29. lemma OAI.CKSInducedSphere.rawContract_add line 162
  30. lemma OAI.CKSInducedSphere.rawContract_sub line 166
  31. lemma OAI.CKSInducedSphere.rawContract_smul line 170
  32. lemma OAI.CKSInducedSphere.first_contribution line 174
  33. lemma OAI.CKSInducedSphere.second_contribution line 189
  34. lemma OAI.CKSInducedSphere.third_contribution line 205
  35. lemma OAI.CKSInducedSphere.trace_contribution line 211
  36. lemma OAI.CKSInducedSphere.rawContract_tfHessian line 223
  37. lemma OAI.CKSInducedSphere.dTangentTrace_formula line 243
  38. lemma OAI.CKSInducedSphere.projectedTraceDeriv_formula line 263
  39. lemma OAI.CKSInducedSphere.rawContract_tfHessian_simplified line 275
  40. lemma OAI.CKSInducedSphere.projected_twice line 282
  41. lemma OAI.CKSInducedSphere.divHessTF_eq line 290
  42. lemma OAI.CKSInducedSphere.hessTF_symm line 325
  43. lemma OAI.CKSInducedSphere.hessTF_normal_left line 338
  44. lemma OAI.CKSInducedSphere.hessTF_projected_left line 351
  45. lemma OAI.CKSInducedSphere.hessTF_trace_zero line 360