showproof: false $ showreason: true $ gcprint: false $ matchfix("{","}"); lcm(m,n) := m*n/gcd(m,n) $ checksymm(expr) := block( [vars], vars: listofvars(expr), return(symm(expr,vars,checkit,expr)) ) $ checkit(expr1,expr2) := block( [temp], if ratsimp(expr1-expr2)=0 then return(true) else return(false) ) $ signseparate():= /* Implicit arguments: left, right, op. */ block([expr], expr: expand(ratsimp(left-right)), left: expr, right: 0, if numberp(expr) and expr<0 then ( right: -left, left: 0, return(true) ), if atom(expr) then return(true), if length(expr)=1 then ( if part(expr,0)="-" then ( right: -left, left: 0 ), return(true) ), if part(expr,0) # "+" then return(true), /* The expression is a sum of terms. Scan these terms and move the positive ones to the left and the negative ones to the right. */ left: 0, right: 0, for term in expr do ( if atom(term) or part(term,0) # "-" then left: left + term else right: right - term ), return(true) ) $ collect():= /* Implicit arguments: left, right, op. */ block( [oldleft,oldright], oldleft: left, oldright: right, signseparate(), if showproof and (ratsimp(left-oldleft)#0 or ratsimp(right-oldright)#0) then ( print("Expanding and collecting terms of the same sign gives:"), disp( op(left,right) ) ) )$ getop(inequal) := block( [op], if atom(inequal) or length(inequal)<2 then (print("Expression is not an inequality:"), error(inequal)), op: part(inequal,0), if op # "<" and op # "<=" and op # ">" and op # ">=" and op # "=" and op # "#" then (print("Expression is not an inequality."), print("Main operator is:", op), error(inequal)), return(op) ) $ homogineq(inequal,varlist):= block([left,right,op,temp,vleft,vright,vl,vr,result], if showproof then showreason: true, op: getop(inequal), left: part(inequal,1), right: part(inequal,2), normalorder(), clearfractions(), result: checkobvious(), if result=true or result=false then return(result), gcdize(), collect(), vleft: vec(left,varlist), vright: vec(right,varlist), /* clear fractions by multiplying both sides by the lcm of the denominators */ vl: apply("+",vleft), vl: denom(ratsimp(vl)), vr: apply("+",vright), vr: denom(ratsimp(vr)), temp: lcm(vl,vr), vleft: temp*vleft, vright: temp*vright, if showreason then ( print("Expressing in terms of symmetric polynomials gives:"), disp( op(apply("+",vleft),apply("+",vright)) ) ), result: majorize(vleft,vright), if not supressbanner and result#true then ( print("left side:",vleft), print("right side:",vright) ), return(result) )$ /* majorize takes two vectors of symmetric sums {a,b,c}, and returns true if the left one majorizes the right one or if the inequality can be proven false. It returns false of right majorizes left and returns notsure if it is not sure. */ majorize(left,right) := block( [lfactor,rfactor,rawright,rawleft,len,result,termsize,p,d,m1,m2,con, leftsum,rightsum,whileresult,change,temp,lcount,lentry, rcount,rentry,res2], /* Heuristic 0: If there is one term on each side, then the result is determined by Muirhead's Theorem. */ if length(left)=1 and length(right)=1 then ( left: first(left), right: first(right), result: major(left,right), if showreason and result=true then print("This result follows from the majorization theorem."), return(result) ), if showreason then print("This follows from the following majorizations:"), whileresult: while length(right)>0 do ( leftsum: apply("+",left), rightsum: apply("+",right), change: false, /* Heuristic 1: See if there is some term on the left that does not majorize anything on the right. If that is the case, then see if we can apply Schur's theorem, either [p+2d,0,0] + [p,d,d] > 2 [p+d,d,0] or [p+d,p+d,0] + [2p,d,d] > 2 [p+d,d,p] */ temp: first(left), temp: temp/numfactor(temp), termsize: length(temp), if termsize=3 then ( for i: 1 thru length(left) do ( lfactor: numfactor(left[i]), rawleft: left[i]/lfactor, result: for j: 1 thru length(right) do ( rfactor: numfactor(right[j]), rawright: right[j]/rfactor, if major(rawleft,rawright)=true then return(true) ), if result#true then ( if part(rawleft,2)=part(rawleft,3) then ( d: part(rawleft,2), p: part(rawleft,1), m1: coeff(leftsum,{p+2*d,0,0}), m2: coeff(rightsum,{p+d,d,0}), if m1#0 and m2#0 then ( con: min(lfactor,m1,entier(m2/2)), leftsum: leftsum-con*{p+2*d,0,0}-con*{p,d,d}, rightsum: rightsum-2*con*{p+d,d,0}, if showreason then disp( con*{p+2*d,0,0}+con*{p,d,d}>=2*con*{p+d,d,0}), left: listerize(leftsum), right: listerize(rightsum), change: true ) else if evenp(p) then ( p: p/2, m1: coeff(leftsum,{p+d,p+d,0}), m2: coeff(rightsum,{p+d,d,p}), if m1#0 and m2#0 then ( con: min(lfactor,m1,entier(m2/2)), leftsum: leftsum-con*{p+d,p+d,0}-con*{2*p,d,d}, rightsum: rightsum-2*con*{p+d,d,p}, if showreason then disp(con*{p+d,p+d,0}+con*{2*p,d,d}>=2*con*{p+d,d,p}), left: listerize(leftsum), right: listerize(rightsum), change: true, return(done) /* want goto(bottom) */ ) ) ) ) ) ), /* Heuristic 2: If there is only one term on the right, then the terms on the left must majorize it away. */ if length(right)=1 then ( len: length(left), right: first(right), rfactor: numfactor(right), rawright: right/rfactor, result: for i: 1 thru len do ( lfactor: numfactor(left[i]), rawleft: left[i]/lfactor, if major(rawleft,rawright)=true then ( con: min(lfactor,rfactor), if showreason then disp(con*rawleft>=con*rawright), rfactor: rfactor-con, rightsum: rightsum - con*rawright, leftsum: leftsum - con*rawleft, change: true, if rfactor<=0 then return(true) ) ), if result=true then return(true) ), left: listerize(leftsum), right: listerize(rightsum), if leftsum=0 and rightsum#0 then return(false), if rightsum=0 then return(true), /* Heuristic 3: If there is a term on the right that is majorized by precisely one term on the left, then we may as well remove that term now. */ for j: 1 thru length(right) do ( rfactor: numfactor(right[j]), rawright: right[j]/rfactor, lcount: 0, for i: 1 thru length(left) do ( lfactor: numfactor(left[i]), rawleft: left[i]/lfactor, if major(rawleft,rawright)=true then ( lcount: lcount+1, lentry: left[i] ) ), if lcount=1 then ( lfactor: numfactor(lentry), rawleft: lentry/lfactor, con: min(lfactor,rfactor), if showreason then disp(con*rawleft>=con*rawright), rightsum: rightsum - con*rawright, leftsum: leftsum - con*rawleft, left: listerize(leftsum), right: listerize(rightsum), change: true, return(done) ) ), if leftsum=0 and rightsum#0 then return(false), if rightsum=0 then return(true), /* Heuristic 4: If there is a term on the left that majorizes precisely one term on the right, then we may as well remove that term now. */ for j: 1 thru length(left) do ( lfactor: numfactor(left[j]), rawleftt: left[j]/lfactor, rcount: 0, for i: 1 thru length(right) do ( rfactor: numfactor(right[i]), rawright: right[i]/rfactor, if major(rawleft,rawright)=true then ( rcount: rcount+1, rentry: right[i] ) ), if rcount=1 then ( rfactor: numfactor(rentry), rawright: rentry/rfactor, con: min(lfactor,rfactor), if showreason then disp(con*rawleft>=con*rawright), rightsum: rightsum - con*rawright, leftsum: leftsum - con*rawleft, left: listerize(leftsum), right: listerize(rightsum), change: true, return(done) ) ), if leftsum=0 and rightsum#0 then return(false), if rightsum=0 then return(true), /* Heuristic 5: If every term on the left majorizes every term on the right, then we can pair them off any way we want. */ result: for j: 1 thru length(right) do ( rfactor: numfactor(right[j]), rawright: right[j]/rfactor, res2: for i: 1 thru length(left) do ( lfactor: numfactor(left[i]), rawleft: left[i]/lfactor, if major(rawleft,rawright)#true then return(false) ), if res2=false then return(false) ), if result#false then ( lfactor: numfactor(left[1]), rawleft: left[1]/lfactor, rfactor: numfactor(right[1]), rawright: right[1]/rfactor, con: min(lfactor,rfactor), if showreason then disp(con*rawleft>=con*rawright), rightsum: rightsum - con*rawright, leftsum: leftsum - con*rawleft, left: listerize(leftsum), right: listerize(rightsum), change: true ), left: listerize(leftsum), right: listerize(rightsum), if leftsum=0 and rightsum#0 then return(false), if rightsum=0 then return(true), /* Heuristic 6: If some term on the left majorizes some term on the right, then we can remove this pair. */ result: for j: 1 thru length(right) do ( rfactor: numfactor(right[j]), rawright: right[j]/rfactor, res2: for i: 1 thru length(left) do ( lfactor: numfactor(left[i]), rawleft: left[i]/lfactor, if major(rawleft,rawright)=true then ( con: min(lfactor,rfactor), if showreason then disp(con*rawleft>=con*rawright), rightsum: rightsum - con*rawright, leftsum: leftsum - con*rawleft, left: listerize(leftsum), right: listerize(rightsum), change: true, return(true) ) ), if res2=true then return(true) ), left: listerize(leftsum), right: listerize(rightsum), if leftsum=0 and rightsum#0 then return(false), if rightsum=0 then return(true), if change=false then return(false) ), if whileresult=true then return(true), if length(right)=0 then return(true), if length(left)>1 and length(right)>1 then return(notsure), return(notyetimplemented) ) $ listerize(expr) := block( [temp], if atom(expr) then (if expr=0 then return([]) else return([expr])), if part(expr,0)="+" then return(maplist(part,expr)) else return([expr]) ) $ /* major takes two symmetric sums, such as {a,b,c} and {d,e,f} and returns true if the left one majorizes the right one. */ major(left,right) := block([lfactor,rfactor,lsum,rsum,len,result], lfactor: numfactor(left), rfactor: numfactor(right), left: left/lfactor, right: right/rfactor, if lfactor < rfactor then return(funnyratio), /* turn {a,b,c} into normal list [a,b,c] */ left: maplist(part,left), right: maplist(part,right), if length(left) # length(right) then display(left,right,lfactor,rfactor), if length(left) # length(right) then return (lengthsdiffer), len: length(left), /* compute the partial sums of each one and check for majorization */ lsum: 0, rsum: 0, result: for i: 1 thru len-1 do ( lsum: lsum + left[i], rsum: rsum + right[i], if lsum= size and expr # 0 then ( print("internal error, expression got larger"), print("term=",term,"ratio=",ratio,"coef=",coef,"co=",co), print("size=",size,"newsize=",newsize,"sym=",sym), display(expr), error(expr) ) ), return(resultvec) ) $ isterm(expr) := block( [temp], if atom(expr) then return(true), if part(expr,0) # "+" then return(true), return(false) )$ symmetrize(term,varlist) := block( [result], cumulate(tem,arg):= result: result+tem, result: 0, symm(term,varlist,cumulate,0), return(result) )$ test(expr) := block([varlist], varlist: listofvars(expr), disp(expr), homogineq(expr,varlist) )$ clearfractions() := /* Implicit arguments: left, right, op. */ block( [dl,dr,prod,pr], left: ratsimp(left), right: ratsimp(right), dl: denom(left), dr: denom(right), prod: lcm(dl,dr), if prod#1 then ( left: num(left)*(prod/dl), right: num(right)*(prod/dr), left: expand(ratsimp(left)), right: expand(ratsimp(right)), if showproof then ( pr: if numberp(prod) then prod else factor(prod), print("Multiplying both sides by",pr,"gives:"), disp( op(left,right) ) ) ) ) $ gcdize() := /* Implicit arguments: left, right, op, showproof. */ block( [temp], if left=0 or right=0 then return(true), temp: gcd(left,right), if numberp(temp) and temp<0 then print("Oops: gcd was negative."), /* Should really confirm that temp is positive. */ if temp#1 then ( left: expand(ratsimp(left/temp)), right: expand(ratsimp(right/temp)), if showproof then ( temp: if numberp(temp) then temp else factor(temp), print("Dividing both sides by", temp, "gives:"), disp( op(left,right) ) ), if not numberp(temp) then collect() ) ) $ normalorder() := /* Returns left, right and op making left side larger than right. */ /* Implicit inputs: left, right, op */ block( [temp], if op = "<" or op = "<=" then ( temp: left, left: right, right: temp, if op="<" then op: ">", if op="<=" then op: ">=" ) ) $ checkobvious() := /* Implicit inputs: left, right, op, showreason. */ block( [temp], collect(), if right=0 and op#"=" then (if showreason then print("This is true because a sum of positive terms must be positive."), return(true) ), if left=0 and right#0 and op#"=" then (if showreason then print("This is false because a sum of positive terms must be positive."), return(false) ), return(undecided) ) $