Dominance in the Family

Global goal:

T0[u_,v_,lambda_]:=(1-lambda)u v+lambda(u+v-1);

T[u_,v_,lambda_]:=Max[0,T0[u,v,lambda]];

hyp=0<lambda<mu&&0<x<1&&0<y<1&&0<u<1&&0<v<1;

goal=T[T[u,v,mu],T[x,y,mu],lambda]≥T[T[x,u,lambda],T[y,v,lambda],mu]

To show:

ForAll[{x,y,u,v},goal]

1. Eliminate the outer maxima.

In general, we have max(0,A)≥max(0,B) iff B≤0||A≥B iff B≤0||A≥B>0:

Clear[A,B];

CylindricalDecomposition[Implies[Max[0,A]≥Max[0,B],B≤0||A≥B],{A,B}]

CylindricalDecomposition[Implies[B≤0||A≥B,B≤0||A≥B>0],{A,B}]

CylindricalDecomposition[Implies[B≤0||A≥B>0,Max[0,A]≥Max[0,B]],{A,B}]

Applied to our particular case, this gives:

A=goal[[1,2]]; B=goal[[2,2]];

ForAll[{x,y,u,v},Implies[hyp,B≤0||A≥B>0]]

2. Eliminate the inner maxima.

X[1]=T0[u,x,lambda];
X[2]=T0[v,y,lambda];
X[3]=T0[u,v,mu];
X[4]=T0[x,y,mu];

A===(1-lambda)Max[0,X[3]]Max[0,X[4]]+lambda(Max[0,X[3]]+Max[0,X[4]]-1)

B===(1-mu)Max[0,X[1]]Max[0,X[2]]+mu(Max[0,X[1]]+Max[0,X[2]]-1)

combs2=Flatten[Outer@@Prepend[Table[{LessEqual,Greater},{2}],u]]/.u->List

combs4=Flatten[Outer@@Prepend[Table[{LessEqual,Greater},{4}],u]]/.u->List

BPart[i_Integer,x_:X]:=And@@(Apply[#[[1]],{#[[2]],0}]&/@Transpose[{combs2[[i]],{x[1],x[2]}}])&&(B/.Table[Max[0,X[j]]:>Evaluate[If[combs2[[i,j]]===LessEqual,0,x[j]]],{j,1,2}])≤0

ABPart[i_Integer,x_:X]:=And@@(Apply[#[[1]],{#[[2]],0}]&/@Transpose[{combs4[[i]],{x[1],x[2],x[3],x[4]}}])&&(A>=B>0)/.Table[Max[0,X[j]]:>Evaluate[If[combs4[[i,j]]===LessEqual,0,x[j]]],{j,1,4}]

New formula with symbolic x:

ForAll[{x,y,u,v},Implies[hyp, Or@@Array[BPart[#,x]&,4]||Or@@Array[ABPart[#,x]&,16]]]

%/.{x->X} (* gives the formula with definitions of X[i] expanded; a bit lengthy... *)

3. Discard redundant clauses

The part coming from B≤0

We confirm the three line equivalence for symbolic x[i]:

line1=(x[1]≤0&&x[2]≤0)||(x[1]>0&&x[2]≤0)||(x[1]≤0&&x[2]>0)||(x[1]>0&&x[2]>0&&T0[x[1],x[2],mu]≤0);
line2=Not[x[1]>0&&x[2]>0]||(x[1]>0&&x[2]>0&&T0[x[1],x[2],mu]≤0);
line3=x[1]≤0||x[2]≤0||T0[x[1],x[2],mu]≤0;

CylindricalDecomposition[Implies[line1,line2],{mu,x[1],x[2]}]

CylindricalDecomposition[Implies[line2,line3],{mu,x[1],x[2]}]

CylindricalDecomposition[Implies[line3,line1],{mu,x[1],x[2]}]

The part coming from A≥B>0

Clause[i_,Phi_]:=hyp&& And@@(Apply[#[[1]],{#[[2]],0}]&/@Transpose[{combs4[[i]],{X[1],X[2],X[3],X[4]}}])&&Phi/.Table[Max[0,X[j]]:>Evaluate[If[combs4[[i,j]]===LessEqual,0,X[j]]],{j,1,4}]

The runtime of the commands below varies between virtually zero and up to 15 sec.

CylindricalDecomposition[Clause[1,A≥0],{lambda,mu,v,x,y,u}]

CylindricalDecomposition[Clause[2,B≥0],{mu,lambda,x,v,u,y}]

CylindricalDecomposition[Clause[3,B≥0],{lambda,mu,y,u,x,v}]

CylindricalDecomposition[Clause[4,B≥0],{lambda,mu,v,x,u,y}]

CylindricalDecomposition[Clause[5,A≥0],{mu,lambda,y,u,x,v}]

CylindricalDecomposition[Clause[6,A≥0],{mu,lambda,x,v,y,u}]

CylindricalDecomposition[Clause[7,A≥0],{lambda,mu,u,y,v,x}]

CylindricalDecomposition[Clause[8,B≥0],{lambda,mu,v,x,y,u}]

CylindricalDecomposition[Clause[9,A≥0],{lambda,mu,y,u,v,x}]

CylindricalDecomposition[Clause[10,A≥0],{mu,lambda,x,v,y,u}]

CylindricalDecomposition[Clause[11,A≥0],{mu,lambda,v,x,u,y}]

CylindricalDecomposition[Clause[12,B≥0],{lambda,mu,x,v,u,y}]

CylindricalDecomposition[Clause[13,A≥0],{lambda,mu,v,x,u,y}]

CylindricalDecomposition[Clause[14,A≥0],{mu,lambda,x,v,y,u}]

CylindricalDecomposition[Clause[15,A≥0],{mu,lambda,u,y,v,x}]

Combination of both parts

ForAll[{x,y,u,v},Implies[hyp,X[1]≤0||X[2]≤0||T0[X[1],X[2],mu]≤0||Clause[16,A≥B>0]]]

4. Apply some logical simplification

Redundance of x[1]  and x[2]

We prove that the negation is false.

Resolve[Exists[{lambda,mu,x,y,u,v},hyp&&X[1]≤0&&T0[X[1],X[2],mu]>0],{},Reals]

Resolve[Exists[{lambda,mu,x,y,u,v},hyp&&X[2]≤0&&T0[X[1],X[2],mu]>0],{},Reals]

Redundance of x[3] and x[4]

We prove again that the negation is false.  These ones take a bit longer than the ones for x[1] and x[2].

Resolve[Exists[{lambda,mu,x,y,u,v},hyp&&T0[X[1],X[2],mu]>0,X[3]≤0],{},Reals]

Resolve[Exists[{lambda,mu,x,y,u,v},hyp&&T0[X[1],X[2],mu]>0,X[4]≤0],{},Reals]

New formula

ForAll[{x,y,u,v},Implies[hyp,T0[X[1],X[2],mu]≤0||T0[X[3],X[4],lambda]-T0[X[1],X[2],mu]≥0]]

5. Apply some algebraic simplifications.

Ineq1=FullSimplify[Together[T0[X[1],X[2],mu]/.{x->1-x,y->1-y,u->1-u,v->1-v}/.v->(v-y)/(1+(lambda-1)y)]]

Ineq2=FullSimplify[(1+(lambda-1)y)Together[(T0[X[3],X[4],lambda]-T0[X[1],X[2],mu])/(mu-lambda)/.{x->1-x,y->1-y,u->1-u,v->1-v}/.v->(v-y)/(1+(lambda-1)y)]]

newhyp=CylindricalDecomposition[hyp/.{v->(v-y)/(1+(lambda-1)y)},{mu,lambda,x,y,u,v}]

New formula:

ForAll[{x,y,u,v},Implies[newhyp,Ineq1≤0||Ineq2≥0]]

Finalization

Negation:

Exists[{x,y,u,v},newhyp&&Ineq1>0&&Ineq2<0]

0<lambda≤1

CylindricalDecomposition[0<lambda≤1&&newhyp &&Ineq2<0,{lambda,mu,x,y,u,v}]

lambda>1

cad=CylindricalDecomposition[lambda>1&&newhyp &&Ineq1>0,{mu,lambda,u,y,v,x}]

cad=CylindricalDecomposition[cad&&Ineq2<0,{mu,lambda,u,y,v,x}];

Take[cad,2]

FullSimplify[FullSimplify[Take[cad,2]]//.Sqrt[u_^i_ v_] -> u^(i/2) Sqrt[v]]

Putting things together

CylindricalDecomposition[0<lambda<mu&&Not[Take[cad,2]],{mu,lambda}]

FullSimplify[FullSimplify[%]//.Sqrt[u_^i_ v_] -> u^(i/2) Sqrt[v]]

Transitivity

prop3[l_,m_]=l==0||m==Infinity||l==m||0<l<m≤17+12Sqrt[2]||(17+12Sqrt[2]<m&&0<l≤((1-3Sqrt[m])/(3-Sqrt[m]))^2)

CylindricalDecomposition[Implies[prop3[a,b]&&prop3[b,c],prop3[a,c]],{a,b,c}]