Initial revision
This commit is contained in:
George Weigt
commit
a1f706b168
4 changed files with 3825 additions and 0 deletions
64
example
Normal file
64
example
Normal file
|
|
@ -0,0 +1,64 @@
|
|||
"Bondi metric..."
|
||||
|
||||
; coordinate system
|
||||
|
||||
(setq x0 u)
|
||||
(setq x1 r)
|
||||
(setq x2 theta)
|
||||
(setq x3 phi)
|
||||
|
||||
; U, V, beta and gamma are functions of u, r and theta
|
||||
|
||||
(setq g_uu (sum
|
||||
(product
|
||||
(V u r theta)
|
||||
(power r -1)
|
||||
(power e (product 2 (beta u r theta)))
|
||||
)
|
||||
(product
|
||||
-1
|
||||
(power (U u r theta) 2)
|
||||
(power r 2)
|
||||
(power e (product 2 (gamma u r theta)))
|
||||
)
|
||||
))
|
||||
|
||||
(setq g_ur (product 2 (power e (product 2 (beta u r theta)))))
|
||||
|
||||
(setq g_utheta (product
|
||||
2
|
||||
(U u r theta)
|
||||
(power r 2)
|
||||
(power e (product 2 (gamma u r theta)))
|
||||
))
|
||||
|
||||
(setq g_thetatheta (product
|
||||
-1
|
||||
(power r 2)
|
||||
(power e (product 2 (gamma u r theta)))
|
||||
))
|
||||
|
||||
(setq g_phiphi (product
|
||||
-1
|
||||
(power r 2)
|
||||
(power e (product -2 (gamma u r theta)))
|
||||
(power (sin theta) 2)
|
||||
))
|
||||
|
||||
; metric tensor
|
||||
|
||||
(setq gdd (sum
|
||||
(product g_uu (tensor u u))
|
||||
(product g_ur (tensor u r))
|
||||
(product g_ur (tensor r u))
|
||||
(product g_utheta (tensor u theta))
|
||||
(product g_utheta (tensor theta u))
|
||||
(product g_thetatheta (tensor theta theta))
|
||||
(product g_phiphi (tensor phi phi))
|
||||
))
|
||||
|
||||
(gr) ; compute g, guu, GAMUDD, RUDDD, RDD, R, GDD, GUD and GUU
|
||||
|
||||
"Is the Einstein tensor GUU divergence-free?"
|
||||
|
||||
(zerop (contract23 (covariant-derivative-of-up-up GUU)))
|
||||
303
robbins.lisp
Normal file
303
robbins.lisp
Normal file
|
|
@ -0,0 +1,303 @@
|
|||
; December 7, 2001
|
||||
|
||||
; See the paper "Solutions of the Robbins Problem" by William McCune.
|
||||
|
||||
; Robbins equation (7)
|
||||
|
||||
(setq E7 (eq (n (sum (n (sum (n x) y)) (n (sum x y)))) y))
|
||||
|
||||
; From this derive the following:
|
||||
|
||||
; n(n(3x)+x)+2x = 2x
|
||||
|
||||
; STEP 10 ---------------------------------------------------------------------
|
||||
|
||||
; with (7), let x be n(x)+y and y be n(x+y)
|
||||
|
||||
(setq E10 (subst Y y E7))
|
||||
|
||||
(setq E10 (subst (sum (n x) y) x E10))
|
||||
|
||||
(setq E10 (eval (subst (n (sum x y)) Y E10)))
|
||||
|
||||
; simplify with (7)
|
||||
|
||||
(setq E10 (eval (subst (caddr E7) (cadr E7) E10)))
|
||||
|
||||
; n(n(n(x+y)+n(x)+y)+y) = n(x+y) ?
|
||||
|
||||
(setq tmp (eq (n (sum (n (sum (n (sum x y)) (n x) y)) y)) (n (sum x y))))
|
||||
|
||||
(equal E10 tmp)
|
||||
|
||||
; STEP 11 ---------------------------------------------------------------------
|
||||
|
||||
; with (7), let y be n(n(x)+y) and x be x+y
|
||||
|
||||
(setq E11 (subst X x E7))
|
||||
|
||||
(setq E11 (subst (n (sum (n x) y)) y E11))
|
||||
|
||||
(setq E11 (eval (subst (sum x y) X E11)))
|
||||
|
||||
; simplify with (7)
|
||||
|
||||
(setq E11 (eval (subst (caddr E7) (cadr E7) E11)))
|
||||
|
||||
; n(n(n(n(x)+y)+x+y)+y) = n(n(x)+y) ?
|
||||
|
||||
(setq tmp (eq (n (sum (n (sum (n (sum (n x) y)) x y)) y)) (n (sum (n x) y))))
|
||||
|
||||
(equal E11 tmp)
|
||||
|
||||
; STEP 29 ---------------------------------------------------------------------
|
||||
|
||||
; with (7), let x be n(n(x)+y)+x+y and y be y
|
||||
|
||||
(setq E29 (eval (subst (sum (n (sum (n x) y)) x y) x E7)))
|
||||
|
||||
; simplify with (11)
|
||||
|
||||
(setq E29 (eval (subst (caddr E11) (cadr E11) E29)))
|
||||
|
||||
; n(n(n(n(x)+y)+x+2y)+n(n(x)+y)) = y ?
|
||||
|
||||
(setq tmp (eq (n (sum (n (sum (n (sum (n x) y)) x y y)) (n (sum (n x) y)))) y))
|
||||
|
||||
(equal E29 tmp)
|
||||
|
||||
; STEP 54 ---------------------------------------------------------------------
|
||||
|
||||
; with (7), let x be n(n(n(x)+y)+x+2y)+n(n(x)+y) and y be z
|
||||
|
||||
(setq E54 (subst z y E7))
|
||||
|
||||
(setq tmp (sum (n (sum x (n (sum y (n x))) (product 2 y))) (n (sum y (n x)))))
|
||||
|
||||
(setq E54 (eval (subst tmp x E54)))
|
||||
|
||||
; simplify with (29)
|
||||
|
||||
(setq E54 (eval (subst (caddr E29) (cadr E29) E54)))
|
||||
|
||||
; n(n(n(n(n(x)+y)+x+2y)+n(n(x)+y)+z)+n(y+z)) = z ?
|
||||
|
||||
(setq tmp (eq (n (sum (n (sum y z)) (n (sum z (n (sum x (n (sum y (n x))) (product 2 y))) (n (sum y (n x))))))) z))
|
||||
|
||||
(equal E54 tmp)
|
||||
|
||||
; STEP 217 --------------------------------------------------------------------
|
||||
|
||||
; with (7), let x be n(n(n(x)+y)+x+2y)+n(n(x)+y)+z and y be n(y+z)
|
||||
|
||||
(setq E217 (subst Y y E7))
|
||||
|
||||
(setq tmp (sum z (n (sum x (n (sum y (n x))) (product 2 y))) (n (sum y (n x)))))
|
||||
|
||||
(setq E217 (subst tmp x E217))
|
||||
|
||||
(setq E217 (eval (subst (n (sum y z)) Y E217)))
|
||||
|
||||
; simplify with E54
|
||||
|
||||
(setq E217 (eval (subst (caddr E54) (cadr E54) E217)))
|
||||
|
||||
; n(n(n(n(n(x)+y)+x+2y)+n(n(x)+y)+n(y+z)+z)+z) = n(y+z) ?
|
||||
|
||||
(setq tmp (eq (n (sum z (n (sum z (n (sum x (n (sum y (n x))) (product 2 y))) (n (sum y z)) (n (sum y (n x))))))) (n (sum y z))))
|
||||
|
||||
(equal E217 tmp)
|
||||
|
||||
; STEP 674 --------------------------------------------------------------------
|
||||
|
||||
; with (7), let y be u and x be n(n(n(n(x)+y)+x+2y)+n(n(x)+y)+n(y+z)+z)+z
|
||||
|
||||
(setq E674 (subst u y E7))
|
||||
|
||||
(setq tmp (sum z (n (sum z (n (sum x (n (sum y (n x))) (product 2 y))) (n (sum y z)) (n (sum y (n x)))))))
|
||||
|
||||
(setq E674 (eval (subst tmp x E674)))
|
||||
|
||||
; simplify with E217
|
||||
|
||||
(setq E674 (eval (subst (caddr E217) (cadr E217) E674)))
|
||||
|
||||
; n(n(n(n(n(n(x)+y)+x+2y)+n(n(x)+y)+n(y+z)+z)+z+u)+n(n(y+z)+u)) = u ?
|
||||
|
||||
(setq tmp (eq (n (sum (n (sum u z (n (sum z (n (sum x (n (sum y (n x))) (product 2 y))) (n (sum y z)) (n (sum y (n x))))))) (n (sum u (n (sum y z)))))) u))
|
||||
|
||||
(equal E674 tmp)
|
||||
|
||||
; STEP 6736 -------------------------------------------------------------------
|
||||
|
||||
; with (10), let x be 3v and y be n(n(3v)+v)+2v
|
||||
|
||||
(setq E10p (subst (product 3 v) x E10))
|
||||
|
||||
(setq tmp (sum (n (sum v (n (product 3 v)))) (product 2 v)))
|
||||
|
||||
(setq E10p (eval (subst tmp y E10p)))
|
||||
|
||||
; with (674), let x be 3v, y be v, z be 2v, and u be n(n(3v)+v)
|
||||
|
||||
(setq E674p (subst (product 3 v) x E674))
|
||||
|
||||
(setq E674p (subst v y E674p))
|
||||
|
||||
(setq E674p (subst (product 2 v) z E674p))
|
||||
|
||||
(setq tmp (n (sum v (n (product 3 v)))))
|
||||
|
||||
(setq E674p (eval (subst tmp u E674p)))
|
||||
|
||||
; simplify with (10')
|
||||
|
||||
(setq E6736 (eval (subst (caddr E10p) (cadr E10p) E674p)))
|
||||
|
||||
; replace v with x
|
||||
|
||||
(setq E6736 (eval (subst x v E6736)))
|
||||
|
||||
; n(n(n(n(3x)+x)+n(3x))+n(n(n(3x)+x)+5x)) = n(n(3x)+x) ?
|
||||
|
||||
(setq tmp (eq (n (sum (n (sum (n (product 3 x)) (n (sum x (n (product 3 x)))))) (n (sum (n (sum x (n (product 3 x)))) (product 5 x))))) (n (sum x (n (product 3 x))))))
|
||||
|
||||
(equal E6736 tmp)
|
||||
|
||||
; STEP 8855 -------------------------------------------------------------------
|
||||
|
||||
; with (7), let x be n(n(3x)+x)+n(3x) and y be n(n(n(3x)+x)+5x)
|
||||
|
||||
(setq E8855 (subst Y y E7))
|
||||
|
||||
(setq tmp (sum (n (product 3 x)) (n (sum x (n (product 3 x))))))
|
||||
|
||||
(setq E8855 (subst tmp x E8855))
|
||||
|
||||
(setq tmp (n (sum (n (sum x (n (product 3 x)))) (product 5 x))))
|
||||
|
||||
(setq E8855 (eval (subst tmp Y E8855)))
|
||||
|
||||
; simplify with (6736)
|
||||
|
||||
(setq E8855 (eval (subst (caddr E6736) (cadr E6736) E8855)))
|
||||
|
||||
; n(n(n(3x)+x)+n(n(n(3x)+x)+n(3x)+n(n(n(3x)+x)+5x))) = n(n(n(3x)+x)+5x) ?
|
||||
|
||||
(setq tmp (eq (n (sum (n (sum x (n (product 3 x)))) (n (sum (n (product 3 x)) (n (sum x (n (product 3 x)))) (n (sum (n (sum x (n (product 3 x)))) (product 5 x))))))) (n (sum (n (sum x (n (product 3 x)))) (product 5 x)))))
|
||||
|
||||
(equal E8855 tmp)
|
||||
|
||||
; with (54), let x be 3x, z be n(3x), and y be x
|
||||
|
||||
(setq tmp (subst (product 3 x) x E54))
|
||||
|
||||
(setq tmp (subst (n (product 3 x)) z tmp))
|
||||
|
||||
(setq tmp (eval (subst x y tmp)))
|
||||
|
||||
; simplify
|
||||
|
||||
(setq E8855 (subst (caddr tmp) (cadr tmp) E8855))
|
||||
|
||||
; flip
|
||||
|
||||
(setq E8855 (eq (caddr E8855) (cadr E8855)))
|
||||
|
||||
; n(n(n(3x)+x)+5x) = n(3x) ?
|
||||
|
||||
(setq tmp (eq (n (sum (n (sum x (n (product 3 x)))) (product 5 x))) (n (product 3 x))))
|
||||
|
||||
(equal E8855 tmp)
|
||||
|
||||
; STEP 8865 -------------------------------------------------------------------
|
||||
|
||||
; with (7), let y be n(n(3x)+x)+2x and x be 3x
|
||||
|
||||
(setq E8865 (subst X x E7))
|
||||
|
||||
(setq tmp (sum (n (sum x (n (product 3 x)))) (product 2 x)))
|
||||
|
||||
(setq E8865 (subst tmp y E8865))
|
||||
|
||||
(setq E8865 (eval (subst (product 3 x) X E8865)))
|
||||
|
||||
; simplify with (8855)
|
||||
|
||||
(setq E8865 (subst (caddr E8855) (cadr E8855) E8865))
|
||||
|
||||
(setq E8865 (eval E8865))
|
||||
|
||||
; n(n(n(n(3x)+x)+n(3x)+2x)+n(3x)) = n(n(3x)+x)+2x ?
|
||||
|
||||
(setq tmp (eq (n (sum (n (product 3 x)) (n (sum (n (product 3 x)) (n (sum x (n (product 3 x)))) (product 2 x))))) (sum (n (sum x (n (product 3 x)))) (product 2 x))))
|
||||
|
||||
(equal E8865 tmp)
|
||||
|
||||
; STEP 8866 -------------------------------------------------------------------
|
||||
|
||||
; with (7), let x be n(n(3x)+x)+4x and y be x
|
||||
|
||||
(setq tmp (sum (n (sum x (n (product 3 x)))) (product 4 x)))
|
||||
|
||||
(setq A2 (subst tmp x E7))
|
||||
|
||||
(setq A2 (eval (subst x y A2)))
|
||||
|
||||
; simplify with (8855)
|
||||
|
||||
(setq A2 (eval (subst (caddr E8855) (cadr E8855) A2)))
|
||||
|
||||
; with (11), let x be 3x and y be x
|
||||
|
||||
(setq A3 (subst (product 3 x) x E11))
|
||||
|
||||
(setq A3 (eval (subst x y A3)))
|
||||
|
||||
; simplify A2 with A3
|
||||
|
||||
(setq E8866 (eval (subst (caddr A3) (cadr A3) A2)))
|
||||
|
||||
; n(n(n(3x)+x)+n(3x)) = x ?
|
||||
|
||||
(setq tmp (eq (n (sum (n (product 3 x)) (n (sum x (n (product 3 x)))))) x))
|
||||
|
||||
(equal E8866 tmp)
|
||||
|
||||
; STEP 8870 -------------------------------------------------------------------
|
||||
|
||||
; with (7), let x = n(n(3x)+x)+n(3x)
|
||||
|
||||
(setq tmp (sum (n (product 3 x)) (n (sum x (n (product 3 x))))))
|
||||
|
||||
(setq E8870 (eval (subst tmp x E7)))
|
||||
|
||||
; simplify with (8866)
|
||||
|
||||
(setq E8870 (eval (subst (caddr E8866) (cadr E8866) E8870)))
|
||||
|
||||
; n(n(n(n(3x)+x)+n(3x)+y)+n(x+y)) = y ?
|
||||
|
||||
(setq tmp (eq (n (sum (n (sum x y)) (n (sum y (n (product 3 x)) (n (sum x (n (product 3 x)))))))) y))
|
||||
|
||||
(equal E8870 tmp)
|
||||
|
||||
; STEP 8871 -------------------------------------------------------------------
|
||||
|
||||
; with (8870), let y be 2x
|
||||
|
||||
(setq tmp (eval (subst (product 2 x) y E8870)))
|
||||
|
||||
; use to simplify (8865)
|
||||
|
||||
(setq E8871 (eval (subst (caddr tmp) (cadr tmp) E8865)))
|
||||
|
||||
; flip
|
||||
|
||||
(setq E8871 (eq (caddr E8871) (cadr E8871)))
|
||||
|
||||
; n(n(3x)+x)+2x = 2x ?
|
||||
|
||||
(setq tmp (eq (sum (n (sum x (n (product 3 x)))) (product 2 x)) (product 2 x)))
|
||||
|
||||
(equal E8871 tmp)
|
||||
612
startup
Normal file
612
startup
Normal file
|
|
@ -0,0 +1,612 @@
|
|||
; lisp reads this file on startup
|
||||
|
||||
(define minus (product -1 arg))
|
||||
(define sqrt (power arg 1/2))
|
||||
(define exp (power e arg))
|
||||
(define complex (sum arg1 (product i arg2)))
|
||||
(define complex-conjugate (eval (subst (product -1 i) i arg)))
|
||||
(define magnitude2 (product arg (complex-conjugate arg)))
|
||||
(define magnitude (sqrt (magnitude2 arg)))
|
||||
(define zerop (equal arg 0))
|
||||
|
||||
(define contract12 (contract 1 2 arg))
|
||||
(define contract13 (contract 1 3 arg))
|
||||
(define contract14 (contract 1 4 arg))
|
||||
(define contract15 (contract 1 5 arg))
|
||||
(define contract16 (contract 1 6 arg))
|
||||
(define contract23 (contract 2 3 arg))
|
||||
(define contract24 (contract 2 4 arg))
|
||||
(define contract25 (contract 2 5 arg))
|
||||
(define contract26 (contract 2 6 arg))
|
||||
(define contract34 (contract 3 4 arg))
|
||||
(define contract35 (contract 3 5 arg))
|
||||
(define contract36 (contract 3 6 arg))
|
||||
(define contract45 (contract 4 5 arg))
|
||||
(define contract46 (contract 4 6 arg))
|
||||
(define contract56 (contract 5 6 arg))
|
||||
|
||||
(define transpose12 (transpose 1 2 arg))
|
||||
(define transpose13 (transpose 1 3 arg))
|
||||
(define transpose14 (transpose 1 4 arg))
|
||||
(define transpose15 (transpose 1 5 arg))
|
||||
(define transpose16 (transpose 1 6 arg))
|
||||
(define transpose23 (transpose 2 3 arg))
|
||||
(define transpose24 (transpose 2 4 arg))
|
||||
(define transpose25 (transpose 2 5 arg))
|
||||
(define transpose26 (transpose 2 6 arg))
|
||||
(define transpose34 (transpose 3 4 arg))
|
||||
(define transpose35 (transpose 3 5 arg))
|
||||
(define transpose36 (transpose 3 6 arg))
|
||||
(define transpose45 (transpose 4 5 arg))
|
||||
(define transpose46 (transpose 4 6 arg))
|
||||
(define transpose56 (transpose 5 6 arg))
|
||||
|
||||
(define caar (car (car arg)))
|
||||
(define cadr (car (cdr arg)))
|
||||
(define cdar (cdr (car arg)))
|
||||
(define cddr (cdr (cdr arg)))
|
||||
|
||||
(define caaar (car (car (car arg))))
|
||||
(define caadr (car (car (cdr arg))))
|
||||
(define cadar (car (cdr (car arg))))
|
||||
(define caddr (car (cdr (cdr arg))))
|
||||
(define cdaar (cdr (car (car arg))))
|
||||
(define cdadr (cdr (car (cdr arg))))
|
||||
(define cddar (cdr (cdr (car arg))))
|
||||
(define cdddr (cdr (cdr (cdr arg))))
|
||||
|
||||
(define caaaar (car (car (car (car arg)))))
|
||||
(define caaadr (car (car (car (cdr arg)))))
|
||||
(define caadar (car (car (cdr (car arg)))))
|
||||
(define caaddr (car (car (cdr (cdr arg)))))
|
||||
(define cadaar (car (cdr (car (car arg)))))
|
||||
(define cadadr (car (cdr (car (cdr arg)))))
|
||||
(define caddar (car (cdr (cdr (car arg)))))
|
||||
(define cadddr (car (cdr (cdr (cdr arg)))))
|
||||
(define cdaaar (cdr (car (car (car arg)))))
|
||||
(define cdaadr (cdr (car (car (cdr arg)))))
|
||||
(define cdadar (cdr (car (cdr (car arg)))))
|
||||
(define cdaddr (cdr (car (cdr (cdr arg)))))
|
||||
(define cddaar (cdr (cdr (car (car arg)))))
|
||||
(define cddadr (cdr (cdr (car (cdr arg)))))
|
||||
(define cdddar (cdr (cdr (cdr (car arg)))))
|
||||
(define cddddr (cdr (cdr (cdr (cdr arg)))))
|
||||
|
||||
(define COS (sum
|
||||
(product 1/2 (exp (product i arg)))
|
||||
(product 1/2 (exp (product -1 i arg)))
|
||||
))
|
||||
|
||||
(define SIN (sum
|
||||
(product -1/2 i (exp (product i arg)))
|
||||
(product 1/2 i (exp (product -1 i arg)))
|
||||
))
|
||||
|
||||
(define COSH (sum
|
||||
(product 1/2 (exp arg))
|
||||
(product 1/2 (exp (product -1 arg)))
|
||||
))
|
||||
|
||||
(define SINH (sum
|
||||
(product 1/2 (exp arg))
|
||||
(product -1/2 (exp (product -1 arg)))
|
||||
))
|
||||
|
||||
(define adjunct (cond
|
||||
(arg5 (adjunct4 arg1 arg2 arg3 arg4 arg5))
|
||||
(arg4 (adjunct3 arg1 arg2 arg3 arg4))
|
||||
(arg3 (adjunct2 arg1 arg2 arg3))
|
||||
(t nil)
|
||||
))
|
||||
|
||||
(define adjunct2 (prog ()
|
||||
(setq temp00 (component arg arg2 arg2))
|
||||
(setq temp01 (component arg arg2 arg3))
|
||||
(setq temp10 (component arg arg3 arg2))
|
||||
(setq temp11 (component arg arg3 arg3))
|
||||
(return (sum
|
||||
(product +1 temp11 (tensor arg2 arg2))
|
||||
(product -1 temp01 (tensor arg2 arg3))
|
||||
(product -1 temp10 (tensor arg3 arg2))
|
||||
(product +1 temp00 (tensor arg3 arg3))
|
||||
))
|
||||
))
|
||||
|
||||
(define adjunct3 (prog ()
|
||||
(setq temp00 (component arg arg2 arg2))
|
||||
(setq temp01 (component arg arg2 arg3))
|
||||
(setq temp02 (component arg arg2 arg4))
|
||||
(setq temp10 (component arg arg3 arg2))
|
||||
(setq temp11 (component arg arg3 arg3))
|
||||
(setq temp12 (component arg arg3 arg4))
|
||||
(setq temp20 (component arg arg4 arg2))
|
||||
(setq temp21 (component arg arg4 arg3))
|
||||
(setq temp22 (component arg arg4 arg4))
|
||||
(return (sum
|
||||
(product +1 temp11 temp22 (tensor arg2 arg2))
|
||||
(product -1 temp21 temp12 (tensor arg2 arg2))
|
||||
(product -1 temp10 temp22 (tensor arg3 arg2))
|
||||
(product +1 temp20 temp12 (tensor arg3 arg2))
|
||||
(product +1 temp10 temp21 (tensor arg4 arg2))
|
||||
(product -1 temp20 temp11 (tensor arg4 arg2))
|
||||
(product -1 temp01 temp22 (tensor arg2 arg3))
|
||||
(product +1 temp21 temp02 (tensor arg2 arg3))
|
||||
(product +1 temp00 temp22 (tensor arg3 arg3))
|
||||
(product -1 temp20 temp02 (tensor arg3 arg3))
|
||||
(product -1 temp00 temp21 (tensor arg4 arg3))
|
||||
(product +1 temp20 temp01 (tensor arg4 arg3))
|
||||
(product +1 temp01 temp12 (tensor arg2 arg4))
|
||||
(product -1 temp11 temp02 (tensor arg2 arg4))
|
||||
(product -1 temp00 temp12 (tensor arg3 arg4))
|
||||
(product +1 temp10 temp02 (tensor arg3 arg4))
|
||||
(product +1 temp00 temp11 (tensor arg4 arg4))
|
||||
(product -1 temp10 temp01 (tensor arg4 arg4))
|
||||
))
|
||||
))
|
||||
|
||||
(define adjunct4 (prog ()
|
||||
(setq temp00 (component arg arg2 arg2))
|
||||
(setq temp01 (component arg arg2 arg3))
|
||||
(setq temp02 (component arg arg2 arg4))
|
||||
(setq temp03 (component arg arg2 arg5))
|
||||
(setq temp10 (component arg arg3 arg2))
|
||||
(setq temp11 (component arg arg3 arg3))
|
||||
(setq temp12 (component arg arg3 arg4))
|
||||
(setq temp13 (component arg arg3 arg5))
|
||||
(setq temp20 (component arg arg4 arg2))
|
||||
(setq temp21 (component arg arg4 arg3))
|
||||
(setq temp22 (component arg arg4 arg4))
|
||||
(setq temp23 (component arg arg4 arg5))
|
||||
(setq temp30 (component arg arg5 arg2))
|
||||
(setq temp31 (component arg arg5 arg3))
|
||||
(setq temp32 (component arg arg5 arg4))
|
||||
(setq temp33 (component arg arg5 arg5))
|
||||
(return (sum
|
||||
(product +1 temp11 temp22 temp33 (tensor arg2 arg2))
|
||||
(product -1 temp11 temp32 temp23 (tensor arg2 arg2))
|
||||
(product -1 temp21 temp12 temp33 (tensor arg2 arg2))
|
||||
(product +1 temp21 temp32 temp13 (tensor arg2 arg2))
|
||||
(product +1 temp31 temp12 temp23 (tensor arg2 arg2))
|
||||
(product -1 temp31 temp22 temp13 (tensor arg2 arg2))
|
||||
(product -1 temp10 temp22 temp33 (tensor arg3 arg2))
|
||||
(product +1 temp10 temp32 temp23 (tensor arg3 arg2))
|
||||
(product +1 temp20 temp12 temp33 (tensor arg3 arg2))
|
||||
(product -1 temp20 temp32 temp13 (tensor arg3 arg2))
|
||||
(product -1 temp30 temp12 temp23 (tensor arg3 arg2))
|
||||
(product +1 temp30 temp22 temp13 (tensor arg3 arg2))
|
||||
(product +1 temp10 temp21 temp33 (tensor arg4 arg2))
|
||||
(product -1 temp10 temp31 temp23 (tensor arg4 arg2))
|
||||
(product -1 temp20 temp11 temp33 (tensor arg4 arg2))
|
||||
(product +1 temp20 temp31 temp13 (tensor arg4 arg2))
|
||||
(product +1 temp30 temp11 temp23 (tensor arg4 arg2))
|
||||
(product -1 temp30 temp21 temp13 (tensor arg4 arg2))
|
||||
(product -1 temp10 temp21 temp32 (tensor arg5 arg2))
|
||||
(product +1 temp10 temp31 temp22 (tensor arg5 arg2))
|
||||
(product +1 temp20 temp11 temp32 (tensor arg5 arg2))
|
||||
(product -1 temp20 temp31 temp12 (tensor arg5 arg2))
|
||||
(product -1 temp30 temp11 temp22 (tensor arg5 arg2))
|
||||
(product +1 temp30 temp21 temp12 (tensor arg5 arg2))
|
||||
(product -1 temp01 temp22 temp33 (tensor arg2 arg3))
|
||||
(product +1 temp01 temp32 temp23 (tensor arg2 arg3))
|
||||
(product +1 temp21 temp02 temp33 (tensor arg2 arg3))
|
||||
(product -1 temp21 temp32 temp03 (tensor arg2 arg3))
|
||||
(product -1 temp31 temp02 temp23 (tensor arg2 arg3))
|
||||
(product +1 temp31 temp22 temp03 (tensor arg2 arg3))
|
||||
(product +1 temp00 temp22 temp33 (tensor arg3 arg3))
|
||||
(product -1 temp00 temp32 temp23 (tensor arg3 arg3))
|
||||
(product -1 temp20 temp02 temp33 (tensor arg3 arg3))
|
||||
(product +1 temp20 temp32 temp03 (tensor arg3 arg3))
|
||||
(product +1 temp30 temp02 temp23 (tensor arg3 arg3))
|
||||
(product -1 temp30 temp22 temp03 (tensor arg3 arg3))
|
||||
(product -1 temp00 temp21 temp33 (tensor arg4 arg3))
|
||||
(product +1 temp00 temp31 temp23 (tensor arg4 arg3))
|
||||
(product +1 temp20 temp01 temp33 (tensor arg4 arg3))
|
||||
(product -1 temp20 temp31 temp03 (tensor arg4 arg3))
|
||||
(product -1 temp30 temp01 temp23 (tensor arg4 arg3))
|
||||
(product +1 temp30 temp21 temp03 (tensor arg4 arg3))
|
||||
(product +1 temp00 temp21 temp32 (tensor arg5 arg3))
|
||||
(product -1 temp00 temp31 temp22 (tensor arg5 arg3))
|
||||
(product -1 temp20 temp01 temp32 (tensor arg5 arg3))
|
||||
(product +1 temp20 temp31 temp02 (tensor arg5 arg3))
|
||||
(product +1 temp30 temp01 temp22 (tensor arg5 arg3))
|
||||
(product -1 temp30 temp21 temp02 (tensor arg5 arg3))
|
||||
(product +1 temp01 temp12 temp33 (tensor arg2 arg4))
|
||||
(product -1 temp01 temp32 temp13 (tensor arg2 arg4))
|
||||
(product -1 temp11 temp02 temp33 (tensor arg2 arg4))
|
||||
(product +1 temp11 temp32 temp03 (tensor arg2 arg4))
|
||||
(product +1 temp31 temp02 temp13 (tensor arg2 arg4))
|
||||
(product -1 temp31 temp12 temp03 (tensor arg2 arg4))
|
||||
(product -1 temp00 temp12 temp33 (tensor arg3 arg4))
|
||||
(product +1 temp00 temp32 temp13 (tensor arg3 arg4))
|
||||
(product +1 temp10 temp02 temp33 (tensor arg3 arg4))
|
||||
(product -1 temp10 temp32 temp03 (tensor arg3 arg4))
|
||||
(product -1 temp30 temp02 temp13 (tensor arg3 arg4))
|
||||
(product +1 temp30 temp12 temp03 (tensor arg3 arg4))
|
||||
(product +1 temp00 temp11 temp33 (tensor arg4 arg4))
|
||||
(product -1 temp00 temp31 temp13 (tensor arg4 arg4))
|
||||
(product -1 temp10 temp01 temp33 (tensor arg4 arg4))
|
||||
(product +1 temp10 temp31 temp03 (tensor arg4 arg4))
|
||||
(product +1 temp30 temp01 temp13 (tensor arg4 arg4))
|
||||
(product -1 temp30 temp11 temp03 (tensor arg4 arg4))
|
||||
(product -1 temp00 temp11 temp32 (tensor arg5 arg4))
|
||||
(product +1 temp00 temp31 temp12 (tensor arg5 arg4))
|
||||
(product +1 temp10 temp01 temp32 (tensor arg5 arg4))
|
||||
(product -1 temp10 temp31 temp02 (tensor arg5 arg4))
|
||||
(product -1 temp30 temp01 temp12 (tensor arg5 arg4))
|
||||
(product +1 temp30 temp11 temp02 (tensor arg5 arg4))
|
||||
(product -1 temp01 temp12 temp23 (tensor arg2 arg5))
|
||||
(product +1 temp01 temp22 temp13 (tensor arg2 arg5))
|
||||
(product +1 temp11 temp02 temp23 (tensor arg2 arg5))
|
||||
(product -1 temp11 temp22 temp03 (tensor arg2 arg5))
|
||||
(product -1 temp21 temp02 temp13 (tensor arg2 arg5))
|
||||
(product +1 temp21 temp12 temp03 (tensor arg2 arg5))
|
||||
(product +1 temp00 temp12 temp23 (tensor arg3 arg5))
|
||||
(product -1 temp00 temp22 temp13 (tensor arg3 arg5))
|
||||
(product -1 temp10 temp02 temp23 (tensor arg3 arg5))
|
||||
(product +1 temp10 temp22 temp03 (tensor arg3 arg5))
|
||||
(product +1 temp20 temp02 temp13 (tensor arg3 arg5))
|
||||
(product -1 temp20 temp12 temp03 (tensor arg3 arg5))
|
||||
(product -1 temp00 temp11 temp23 (tensor arg4 arg5))
|
||||
(product +1 temp00 temp21 temp13 (tensor arg4 arg5))
|
||||
(product +1 temp10 temp01 temp23 (tensor arg4 arg5))
|
||||
(product -1 temp10 temp21 temp03 (tensor arg4 arg5))
|
||||
(product -1 temp20 temp01 temp13 (tensor arg4 arg5))
|
||||
(product +1 temp20 temp11 temp03 (tensor arg4 arg5))
|
||||
(product +1 temp00 temp11 temp22 (tensor arg5 arg5))
|
||||
(product -1 temp00 temp21 temp12 (tensor arg5 arg5))
|
||||
(product -1 temp10 temp01 temp22 (tensor arg5 arg5))
|
||||
(product +1 temp10 temp21 temp02 (tensor arg5 arg5))
|
||||
(product +1 temp20 temp01 temp12 (tensor arg5 arg5))
|
||||
(product -1 temp20 temp11 temp02 (tensor arg5 arg5))
|
||||
))
|
||||
))
|
||||
|
||||
(define determinant (cond
|
||||
(arg5 (determinant4 arg1 arg2 arg3 arg4 arg5))
|
||||
(arg4 (determinant3 arg1 arg2 arg3 arg4))
|
||||
(arg3 (determinant2 arg1 arg2 arg3))
|
||||
(t nil)
|
||||
))
|
||||
|
||||
(define determinant2 (prog ()
|
||||
(setq temp00 (component arg arg2 arg2))
|
||||
(setq temp01 (component arg arg2 arg3))
|
||||
(setq temp10 (component arg arg3 arg2))
|
||||
(setq temp11 (component arg arg3 arg3))
|
||||
(return (sum
|
||||
(product +1 temp00 temp11)
|
||||
(product -1 temp01 temp10)
|
||||
))
|
||||
))
|
||||
|
||||
(define determinant3 (prog ()
|
||||
(setq temp00 (component arg arg2 arg2))
|
||||
(setq temp01 (component arg arg2 arg3))
|
||||
(setq temp02 (component arg arg2 arg4))
|
||||
(setq temp10 (component arg arg3 arg2))
|
||||
(setq temp11 (component arg arg3 arg3))
|
||||
(setq temp12 (component arg arg3 arg4))
|
||||
(setq temp20 (component arg arg4 arg2))
|
||||
(setq temp21 (component arg arg4 arg3))
|
||||
(setq temp22 (component arg arg4 arg4))
|
||||
(return (sum
|
||||
(product +1 temp00 temp11 temp22)
|
||||
(product -1 temp00 temp21 temp12)
|
||||
(product -1 temp10 temp01 temp22)
|
||||
(product +1 temp10 temp21 temp02)
|
||||
(product +1 temp20 temp01 temp12)
|
||||
(product -1 temp20 temp11 temp02)
|
||||
))
|
||||
))
|
||||
|
||||
(define determinant4 (prog ()
|
||||
(setq temp00 (component arg arg2 arg2))
|
||||
(setq temp01 (component arg arg2 arg3))
|
||||
(setq temp02 (component arg arg2 arg4))
|
||||
(setq temp03 (component arg arg2 arg5))
|
||||
(setq temp10 (component arg arg3 arg2))
|
||||
(setq temp11 (component arg arg3 arg3))
|
||||
(setq temp12 (component arg arg3 arg4))
|
||||
(setq temp13 (component arg arg3 arg5))
|
||||
(setq temp20 (component arg arg4 arg2))
|
||||
(setq temp21 (component arg arg4 arg3))
|
||||
(setq temp22 (component arg arg4 arg4))
|
||||
(setq temp23 (component arg arg4 arg5))
|
||||
(setq temp30 (component arg arg5 arg2))
|
||||
(setq temp31 (component arg arg5 arg3))
|
||||
(setq temp32 (component arg arg5 arg4))
|
||||
(setq temp33 (component arg arg5 arg5))
|
||||
(return (sum
|
||||
(product +1 temp00 temp11 temp22 temp33)
|
||||
(product -1 temp00 temp11 temp32 temp23)
|
||||
(product -1 temp00 temp21 temp12 temp33)
|
||||
(product +1 temp00 temp21 temp32 temp13)
|
||||
(product +1 temp00 temp31 temp12 temp23)
|
||||
(product -1 temp00 temp31 temp22 temp13)
|
||||
(product -1 temp10 temp01 temp22 temp33)
|
||||
(product +1 temp10 temp01 temp32 temp23)
|
||||
(product +1 temp10 temp21 temp02 temp33)
|
||||
(product -1 temp10 temp21 temp32 temp03)
|
||||
(product -1 temp10 temp31 temp02 temp23)
|
||||
(product +1 temp10 temp31 temp22 temp03)
|
||||
(product +1 temp20 temp01 temp12 temp33)
|
||||
(product -1 temp20 temp01 temp32 temp13)
|
||||
(product -1 temp20 temp11 temp02 temp33)
|
||||
(product +1 temp20 temp11 temp32 temp03)
|
||||
(product +1 temp20 temp31 temp02 temp13)
|
||||
(product -1 temp20 temp31 temp12 temp03)
|
||||
(product -1 temp30 temp01 temp12 temp23)
|
||||
(product +1 temp30 temp01 temp22 temp13)
|
||||
(product +1 temp30 temp11 temp02 temp23)
|
||||
(product -1 temp30 temp11 temp22 temp03)
|
||||
(product -1 temp30 temp21 temp02 temp13)
|
||||
(product +1 temp30 temp21 temp12 temp03)
|
||||
))
|
||||
))
|
||||
|
||||
; P (x) = 1
|
||||
; 0
|
||||
;
|
||||
; P (x) = x
|
||||
; 1
|
||||
;
|
||||
; n P (x) = (2n - 1) x P (x) - (n - 1) P (x)
|
||||
; n n-1 n-2
|
||||
;
|
||||
; (legendre x n)
|
||||
|
||||
(define legendre (cond
|
||||
((equal arg2 0) 1)
|
||||
((equal arg2 1) arg1)
|
||||
(t (product (power arg2 -1) (sum
|
||||
(product (sum (product 2 arg2) -1) arg1 (legendre arg1 (sum arg2 -1)))
|
||||
(product -1 (sum arg2 -1) (legendre arg1 (sum arg2 -2)))
|
||||
)))
|
||||
))
|
||||
|
||||
(define nth-derivative (cond
|
||||
((zerop arg3) arg1)
|
||||
(t (derivative (nth-derivative arg1 arg2 (sum arg3 -1)) arg2))
|
||||
))
|
||||
|
||||
; L (x, a) = 1
|
||||
; 0
|
||||
;
|
||||
; L (x, a) = 1 + a - x
|
||||
; 1
|
||||
;
|
||||
; n L (x, a) = (2n + a - 1 - x) L (x, a) + (1 - n - a) L (x, a)
|
||||
; n n-1 n-2
|
||||
;
|
||||
; (laguerre x n a)
|
||||
;
|
||||
; only works for n <= 6 due to 32-bit integers
|
||||
|
||||
(define laguerre (cond
|
||||
((equal arg2 0) 1)
|
||||
((equal arg2 1) (sum 1 arg3 (product -1 arg1)))
|
||||
(t (product (power arg2 -1) (sum
|
||||
(product (sum (product 2 arg2) arg3 -1 (product -1 arg1)) (laguerre arg1 (sum arg2 -1) arg3))
|
||||
(product (sum 1 (product -1 arg2) (product -1 arg3)) (laguerre arg1 (sum arg2 -2) arg3))
|
||||
)))
|
||||
))
|
||||
|
||||
; -a x n n n+a -x
|
||||
; L(x, n, a) = (1/n!) x e (d /dx ) (x e )
|
||||
|
||||
(define laguerre2 (product
|
||||
(power (factorial arg2) -1)
|
||||
(power arg1 (product -1 arg3))
|
||||
(exp arg)
|
||||
(nth-derivative
|
||||
(product (power arg1 (sum arg2 arg3)) (exp (product -1 arg)))
|
||||
arg1
|
||||
arg2
|
||||
)
|
||||
))
|
||||
|
||||
(define absval (cond
|
||||
((not (numberp arg)) nil)
|
||||
((lessp arg 0) (product -1 arg))
|
||||
(t arg)
|
||||
))
|
||||
|
||||
(define factorial (cond
|
||||
((zerop arg) 1)
|
||||
(t (product arg (factorial (sum arg -1))))
|
||||
))
|
||||
|
||||
(define laplacian (sum
|
||||
(product
|
||||
(power r -2)
|
||||
(derivative (product (power r 2) (derivative arg r)) r)
|
||||
)
|
||||
(product
|
||||
(power r -2)
|
||||
(power (sin theta) -1)
|
||||
(derivative (product (sin theta) (derivative arg theta)) theta)
|
||||
)
|
||||
(product
|
||||
(power r -2)
|
||||
(power (sin theta) -2)
|
||||
(derivative (derivative arg phi) phi)
|
||||
)
|
||||
))
|
||||
|
||||
; arg1=n arg2=x
|
||||
|
||||
(define hermite (product
|
||||
(power -1 arg1)
|
||||
(power e (power arg2 2))
|
||||
(nth-derivative (power e (product -1 (power arg2 2))) arg2 arg1)
|
||||
))
|
||||
|
||||
; generic metric
|
||||
|
||||
(setq gdd (sum
|
||||
(product (g00) (tensor x0 x0))
|
||||
(product (g11) (tensor x1 x1))
|
||||
(product (g22) (tensor x2 x2))
|
||||
(product (g33) (tensor x3 x3))
|
||||
))
|
||||
|
||||
(setq eta (sum
|
||||
(product -1 (tensor x0 x0))
|
||||
(product +1 (tensor x1 x1))
|
||||
(product +1 (tensor x2 x2))
|
||||
(product +1 (tensor x3 x3))
|
||||
))
|
||||
|
||||
(define epsilon (sum
|
||||
(product +1 (tensor x0 x1 x2 x3)) ; 1
|
||||
(product -1 (tensor x0 x1 x3 x2)) ; 2
|
||||
(product -1 (tensor x0 x2 x1 x3)) ; 3
|
||||
(product +1 (tensor x0 x2 x3 x1)) ; 4
|
||||
(product +1 (tensor x0 x3 x1 x2)) ; 5
|
||||
(product -1 (tensor x0 x3 x2 x1)) ; 6
|
||||
(product -1 (tensor x1 x0 x2 x3)) ; 7
|
||||
(product +1 (tensor x1 x0 x3 x2)) ; 8
|
||||
(product +1 (tensor x1 x2 x0 x3)) ; 9
|
||||
(product -1 (tensor x1 x2 x3 x0)) ; 10
|
||||
(product -1 (tensor x1 x3 x0 x2)) ; 11
|
||||
(product +1 (tensor x1 x3 x2 x0)) ; 12
|
||||
(product +1 (tensor x2 x0 x1 x3)) ; 13
|
||||
(product -1 (tensor x2 x0 x3 x1)) ; 14
|
||||
(product -1 (tensor x2 x1 x0 x3)) ; 15
|
||||
(product +1 (tensor x2 x1 x3 x0)) ; 16
|
||||
(product +1 (tensor x2 x3 x0 x1)) ; 17
|
||||
(product -1 (tensor x2 x3 x1 x0)) ; 18
|
||||
(product -1 (tensor x3 x0 x1 x2)) ; 19
|
||||
(product +1 (tensor x3 x0 x2 x1)) ; 20
|
||||
(product +1 (tensor x3 x1 x0 x2)) ; 21
|
||||
(product -1 (tensor x3 x1 x2 x0)) ; 22
|
||||
(product -1 (tensor x3 x2 x0 x1)) ; 23
|
||||
(product +1 (tensor x3 x2 x1 x0)) ; 24
|
||||
))
|
||||
|
||||
(define gradient (sum
|
||||
(product (derivative arg x0) (tensor x0))
|
||||
(product (derivative arg x1) (tensor x1))
|
||||
(product (derivative arg x2) (tensor x2))
|
||||
(product (derivative arg x3) (tensor x3))
|
||||
))
|
||||
|
||||
; compute g, guu, GAMUDD, RUDDD, RDD, R, GDD, GUD and GUU from gdd
|
||||
|
||||
(define gr (prog (tmp tmp1 tmp2)
|
||||
(setq g (determinant gdd x0 x1 x2 x3))
|
||||
(setq guu (product (power g -1) (adjunct gdd x0 x1 x2 x3)))
|
||||
; connection coefficients
|
||||
(setq tmp (gradient gdd))
|
||||
(setq GAMUDD (contract23 (product 1/2 guu (sum
|
||||
tmp
|
||||
(transpose23 tmp)
|
||||
(product -1 (transpose12 (transpose23 tmp)))
|
||||
))))
|
||||
; riemann tensor
|
||||
(setq tmp1 (gradient GAMUDD))
|
||||
(setq tmp2 (contract24 (product GAMUDD GAMUDD)))
|
||||
(setq RUDDD (sum
|
||||
(transpose34 tmp1)
|
||||
(product -1 tmp1)
|
||||
(transpose23 tmp2)
|
||||
(product -1 (transpose34 (transpose23 tmp2)))
|
||||
))
|
||||
(setq RDD (contract13 RUDDD)) ; ricci tensor
|
||||
(setq R (contract12 (contract23 (product guu RDD)))) ; ricci scalar
|
||||
(setq GDD (sum RDD (product -1/2 gdd R))) ; einstein tensor
|
||||
(setq GUD (contract23 (product guu GDD))) ; raise 1st index
|
||||
(setq GUU (contract23 (product GUD guu))) ; raise 2nd index
|
||||
))
|
||||
|
||||
; covariant derivative of a vector
|
||||
|
||||
(define covariant-derivative (sum
|
||||
(gradient arg)
|
||||
(contract13 (product arg GAMUDD))
|
||||
))
|
||||
|
||||
(define covariant-derivative-of-up-up (prog (tmp)
|
||||
(setq tmp (product arg GAMUDD))
|
||||
(return (sum
|
||||
(gradient arg)
|
||||
(transpose12 (contract14 tmp))
|
||||
(contract24 tmp)
|
||||
))
|
||||
))
|
||||
|
||||
(define covariant-derivative-of-up-down (prog (tmp)
|
||||
(setq tmp (product arg GAMUDD))
|
||||
(return (sum
|
||||
(gradient arg)
|
||||
(transpose12 (contract14 tmp))
|
||||
(product -1 (contract23 tmp))
|
||||
))
|
||||
))
|
||||
|
||||
(define covariant-derivative-of-down-down (prog (tmp)
|
||||
(setq tmp (product arg GAMUDD))
|
||||
(return (sum
|
||||
(gradient arg)
|
||||
(product -1 (transpose12 (contract13 tmp)))
|
||||
(product -1 (contract23 tmp))
|
||||
))
|
||||
))
|
||||
|
||||
(define add-integral (prog (tmp)
|
||||
(setq tmp arg)
|
||||
(setq tmp (subst meta-a a tmp))
|
||||
(setq tmp (subst meta-n n tmp))
|
||||
(setq tmp (subst meta-x x tmp))
|
||||
(setq integral-list (append integral-list (cons tmp nil)))
|
||||
))
|
||||
|
||||
(add-integral (list
|
||||
'(power x -1)
|
||||
'(log x)
|
||||
))
|
||||
|
||||
(add-integral (list
|
||||
'(power x n)
|
||||
'(product (power (sum n 1) -1) (power x (sum n 1)))
|
||||
'(numberp n)
|
||||
'(not (equal n -1))
|
||||
))
|
||||
|
||||
(add-integral (list
|
||||
'(power e (product a x))
|
||||
'(product (power a -1) (power e (product a x)))
|
||||
))
|
||||
|
||||
; n ax -1 n ax -1 n-1 ax
|
||||
; x e -> a x e - n a (integral x e )
|
||||
;
|
||||
; integer n, n > 0
|
||||
|
||||
(add-integral (list
|
||||
'(product
|
||||
(power x n)
|
||||
(power e (product a x))
|
||||
)
|
||||
'(sum
|
||||
(product
|
||||
(power a -1)
|
||||
(power x n)
|
||||
(power e (product a x))
|
||||
)
|
||||
(product
|
||||
-1
|
||||
n
|
||||
(power a -1)
|
||||
(integral
|
||||
(product
|
||||
(power x (sum n -1))
|
||||
(power e (product a x))
|
||||
)
|
||||
x
|
||||
)
|
||||
)
|
||||
)
|
||||
'(integerp n)
|
||||
'(greaterp n 0)
|
||||
))
|
||||
Loading…
Add table
Reference in a new issue