Cheat Sheet J - Verification

Pensieve header: Cheat Sheet $J$ Verification; continues pensieve://2013-03/; continued pensieve://2013-12/.

SetDirectory["C:\\drorbn\\AcademicPensieve\\2013-04"];
<< FreeLie.m;
tm[u_,v_,w_] := LieMorphism[⟨u⟩->⟨w⟩, ⟨v⟩->⟨w⟩];
CC[u_, γ_LieSeries] := LieMorphism[u -> Ad[γ][u]];
(Subscript[CC, u_])[γ_] := CC[u,γ];
RC[u_, γ_LieSeries, ub_][ser_] := StableApply[LieMorphism[⟨u⟩ -> Ad[γ][⟨ub⟩]], ser];
RC[u_, γ_LieSeries][ser_] := ser // RC[u, γ,⟨υ⟩] // LieMorphism[⟨υ⟩->⟨u⟩];
(Subscript[RC, u_])[γ_] := RC[u,γ];
Print /@ {{t=⟨"t"⟩, u=⟨"u"⟩, v=⟨"v"⟩, w=⟨"w"⟩},
α = RandomLieSeries[{t,u,v}],
β = RandomLieSeries[{t,u,v}],
γ = RandomLieSeries[{t,u,v}]
};
$SeriesShowDegree=3; $SeriesCompareDegree = 6;

ad[u_, γ_LieSeries] := LieDerivation[u -> b[γ, u]];
(Subscript[ad, u_])[γ_] := ad[u,γ];
ϵ /: (ϵ^2)=0;

Some preliminary testing

(α // (Subscript[RC, u])[γ] // (Subscript[CC, u])[-γ])≡α

(α // (Subscript[RC, u])[γ] // (Subscript[RC, u])[-γ//(Subscript[RC, u])[γ]])≡α

The Definition of J

J[u_, γ_] := Module[{s},(∫_0^1)(γ // (Subscript[RC, u])[s γ] // (Subscript[div, u]) // (Subscript[CC, u])[-s γ])\[DifferentialD]s];
(Subscript[J, u_])[γ_] := J[u,γ];

(Subscript[J, u])[α][{4}]

The (Subscript[J, uv]) equation

Print /@ {
0 -> {α, β},
1 -> (t1=(Subscript[J, u])[α]+((Subscript[J, v])[β // (Subscript[RC, u])[α]] // (Subscript[CC, u])[-α])),
2 -> (t2=(Subscript[J, v])[β]+((Subscript[J, u])[α // (Subscript[RC, v])[β]] // (Subscript[CC, v])[-β])),
3->  t1≡t2
};

Print /@ {
0 -> {α, β},
1 -> (t1=(Subscript[J, u])[α]+((Subscript[J, v])[β // (Subscript[RC, u])[s α]] // (Subscript[CC, u])[-s α])),
2 -> (t2=(Subscript[J, v])[β]+((Subscript[J, u])[α // (Subscript[RC, v])[s β]] // (Subscript[CC, v])[-s β])),
3->  t1≡t2
};

Print /@ {
0 -> {α, β},
1 -> (t1=(Subscript[J, u])[α]),
2 -> (t2=(Subscript[J, u])[α // (Subscript[RC, v])[β]] // (Subscript[CC, v])[-β]),
3->  t1≡t2
};

Print /@ {
0 -> {α, β},
1 -> (t1=(Subscript[J, u])[α] // (Subscript[RC, u])[α] // (Subscript[RC, v])[β] // (Subscript[RC, u])[α]),
2 -> (t2=(Subscript[J, u])[α // (Subscript[RC, v])[β]] // (Subscript[RC, u])[α // (Subscript[RC, v])[β]]),
3->  t1≡t2
};

The t equation

Print /@ {
0 -> γ,
1 -> (t1=J[w, γ // tm[u,v,w]]),
2 -> (t2=(Subscript[J, u])[γ] // tm[u,v,w]),
3 -> (t3=(Subscript[J, v])[γ // (Subscript[RC, u])[γ]] // (Subscript[CC, u])[-γ] // tm[u,v,w]),
4 -> t1≡t2+t3
};

Print /@ {
0 -> {γ, γw =  γ // tm[u,v,w]},
1 -> (t1=J[w, γw] // (Subscript[RC, w])[γw]),
2 -> (t2=(Subscript[J, u])[γ] // tm[u,v,w] // (Subscript[RC, w])[γw]),
3 -> (t3=(Subscript[J, v])[γ // (Subscript[RC, u])[γ]] // (Subscript[RC, v])[γ // (Subscript[RC, u])[γ]] // tm[u,v,w]),
4 -> t1≡t2+t3
};

Splitting the t equation

Print /@ {
0 -> {γ, γw =  γ // tm[u,v,w]},
1 -> (t1=γw// (Subscript[RC, w])[s γw]),
2 -> (t2=γ // (Subscript[RC, u])[s γ] // (Subscript[RC, v])[s γ // (Subscript[RC, u])[s γ]] // tm[u,v,w]),
3 -> t1≡t2,
4 -> (t3=γ // (Subscript[RC, u])[s γ] // (Subscript[RC, v])[s γ // (Subscript[RC, u])[s γ]]// tm[u,v,w] // (Subscript[div, w])),
5 -> (t4=γ // (Subscript[RC, u])[s γ] // (Subscript[RC, v])[s γ // (Subscript[RC, u])[s γ]]// (Subscript[div, u]) // tm[u,v,w]),
6 -> (t5=γ // (Subscript[RC, u])[s γ] // (Subscript[RC, v])[s γ // (Subscript[RC, u])[s γ]]// (Subscript[div, v]) // tm[u,v,w]),
7 -> t3≡t4+t5,
8 -> (t6 = (∫_0^1)(t3 // (Subscript[CC, w])[-s γw])\[DifferentialD]s),
9 -> t6≡(Subscript[J, w])[γw],
10 -> (t7=(∫_0^1)(t4 // (Subscript[CC, w])[-s γw])\[DifferentialD]s),
11 -> (t8=(∫_0^1)(t5 // (Subscript[CC, w])[-s γw])\[DifferentialD]s),
12 -> t6≡t7+t8,
((Subscript[J, u])[γ] // tm[u,v,w] // (Subscript[RC, w])[γw])≡(t7 // (Subscript[RC, w])[γw])
};

The h equation

Print /@ {
1 -> (t1=J[u, BCH[α, β]]),
2 -> (t2=J[u,α]),
3 -> (t3=J[u,β//RC[u,α]]//CC[u,-α]),
4 -> t1≡t2+t3
};

h and S

(Plus[
(Subscript[J, u])[γ]//(Subscript[RC, u])[γ],
(Subscript[J, u])[-γ//(Subscript[RC, u])[γ]]
] // (Subscript[RC, u])[-γ//(Subscript[RC, u])[γ]]) @ {6}

The meaning(s) of RC

Print /@ {
1 -> α,
2 -> (t1=α // CC[u, γ] // RC[u, -γ]),
3 -> α≡t1
};

Print /@ {
1 -> α,
2 -> (t1= α // CC[u, γ // RC[u, γ]]),
3 -> (t2= α // RC[u, γ]),
4 -> t1≡t2
};

(Subscript[C, u])(Subscript[C, v]) and (Subscript[RC, u])(Subscript[RC, v])

Print /@ {
1 -> {α, β, γ},
2 -> (t1=γ // (Subscript[CC, u])[α // (Subscript[RC, v])[-β]] // (Subscript[CC, v])[β]),
3 -> (t2=γ // (Subscript[CC, v])[β // (Subscript[RC, u])[-α]] // (Subscript[CC, u])[α]),
4 -> t1≡t2
};

Print /@ {
1 -> {α, β, γ},
2 -> (t1=γ // (Subscript[RC, u])[α] // (Subscript[RC, v])[β // (Subscript[RC, u])[α]]),
3 -> (t2=γ // (Subscript[RC, v])[β] // (Subscript[RC, u])[α // (Subscript[RC, v])[β]]),
4 -> t1≡t2
};

div property uv

Print /@ {
0 -> {α, β},
1 -> (t1=(Subscript[div, u])[α] // (Subscript[ad, v])[β]),
2 -> (t2=(Subscript[div, v])[β] // (Subscript[ad, u])[α]),
3 -> (t3=MakeCWSeries[0]),
4 -> (t4=(Subscript[div, u])[α//(Subscript[ad, v])[β]]),
5 -> (t5=(Subscript[div, v])[β//(Subscript[ad, u])[α]]),
6 -> t1-t2≡t3+t4-t5
};

div property uu

Print /@ {
0 -> {α, β},
1 -> (t1=(Subscript[div, u])[α] // (Subscript[ad, u])[β]),
2 -> (t2=(Subscript[div, u])[β] // (Subscript[ad, u])[α]),
3 -> (t3=(Subscript[div, u])[b[α,β]]),
4 -> (t4=(Subscript[div, u])[α//(Subscript[ad, u])[β]]),
5 -> (t5=(Subscript[div, u])[β//(Subscript[ad, u])[α]]),
6 -> t1-t2≡t3+t4-t5
};

The differential of BCH

Print /@ {
1 -> (bch=BCH[u,v]),
2 -> ((BCH[u+ϵ t, v+ϵ w]-bch)/ϵ),
3 -> (t1=((BCH[u+ϵ t, v+ϵ w]-bch)/ϵ) // adSeries[((1-(E^(-ad)))/ad), bch]),
4 -> (t2=t // adSeries[((1-(E^(-ad)))/ad),u] // Ad[-v]),
5 -> (t3=w // adSeries[((1-(E^(-ad)))/ad),v])
};
t1 ≡ t2+t3

The differential of C

Print /@ {
0 -> {α, β, γ},
1 -> (t1=(((γ // CC[u, α+ϵ β]) - (γ // CC[u, α]) )/ϵ)),
2 -> (t2=γ // ad[u, adSeries[(((E^ad)-1)/ad),α][β] // RC[u, -α]] // CC[u, α]),
t1 ≡ t2
};

The differential of RC

Print /@ {
0 -> {α, β, γ},
1 -> (t1=(((γ // RC[u, α+ϵ β]) - (γ // RC[u, α]) )/ϵ)),
2 -> (t2=γ // RC[u, α] // ad[u, adSeries[((1-(E^(-ad)))/ad),α][β] // RC[u, α]]),
t1 ≡ t2
};

The differential of J

Print /@ {
0 -> {α, β},
1 -> (t0=((J[u,α+ϵ β]-J[u,α])/ϵ)),
2 -> (t1=(∫_0^1)(div[u, β // RC[u,s α]] // CC[u,-s α])\[DifferentialD]s),
3 -> (t2=(∫_0^1)(s div[u, α // RC[u,s α] // ad[u, β//adSeries[((1-(E^(-s ad)))/(s ad)), α]//RC[u, s α]]] // CC[u,-s α])\[DifferentialD]s),
4 -> (t3=(∫_0^1)(s div[u, α // RC[u,s α]] // ad[u, β//adSeries[((1-(E^(-s ad)))/(s ad)), α]//RC[u, s α]] // CC[u,-s α])\[DifferentialD]s),
t0 ≡ t1+t2-t3
};

Print /@ {
0 -> {α, β};
1 -> (t0=((J[u,α+ϵ β]-J[u,α])/ϵ)),
2 -> (t1=(∫_0^1)(div[u, β // RC[u,s α]] // CC[u,-s α])\[DifferentialD]s),
3 -> (t2=(∫_0^1)(div[u, β//adSeries[((1-(E^(-s ad)))/ad), α]//RC[u, s α] // ad[u, α // RC[u,s α]]] // CC[u,-s α])\[DifferentialD]s),
4 -> (t3=(∫_0^1)(div[u, β//adSeries[((1-(E^(-s ad)))/ad), α]//RC[u, s α]] // ad[u, α // RC[u,s α]] // CC[u,-s α])\[DifferentialD]s),
5 -> (t4=(∫_0^1)(div[u, b[α // RC[u,s α], β//adSeries[((1-(E^(-s ad)))/ad), α]//RC[u, s α]]] // CC[u,-s α])\[DifferentialD]s),
t0 ≡ t1+t2-t3-t4
};

Print /@ {
0 -> {α, β};
1 -> (t0=((J[u,α+ϵ β]-J[u,α])/ϵ)),
2 -> (t1=(∫_0^1)(div[u, β // RC[u,s α]] // CC[u,-s α])\[DifferentialD]s),
3 -> (t2=(∫_0^1)(div[u, β//adSeries[((1-(E^(-s ad)))/ad), α]//RC[u, s α] // ad[u, α // RC[u,s α]]] // CC[u,-s α])\[DifferentialD]s),
4 -> (t3=(∫_0^1)(div[u, β//adSeries[((1-(E^(-s ad)))/ad), α]//RC[u, s α]] // ad[u, α // RC[u,s α]] // CC[u,-s α])\[DifferentialD]s),
5 -> (t4=(∫_0^1)(div[u, b[α, β//adSeries[((1-(E^(-s ad)))/ad), α]]// RC[u,s α]] // CC[u,-s α])\[DifferentialD]s),
t0 ≡ t1+t2-t3-t4
};

Print /@ {
0 -> {α, β};
1 -> (t0=((J[u,α+ϵ β]-J[u,α])/ϵ)),
2 -> (t1=(∫_0^1)(div[u, β // RC[u,s α]] // CC[u,-s α])\[DifferentialD]s),
3 -> (t2=(∫_0^1)(div[u, β//adSeries[((1-(E^(-s ad)))/ad), α]//RC[u, s α] // ad[u, α // RC[u,s α]]] // CC[u,-s α])\[DifferentialD]s),
4 -> (t3=(∫_0^1)(div[u, β//adSeries[((1-(E^(-s ad)))/ad), α]//RC[u, s α]] // ad[u, α // RC[u,s α]] // CC[u,-s α])\[DifferentialD]s),
5 -> (t4=(∫_0^1)(div[u, β//adSeries[1-(E^(-s ad)), α]// RC[u,s α]] // CC[u,-s α])\[DifferentialD]s),
t0 ≡ t1+t2-t3-t4
};

Print /@ {
0 -> {α, β};
1 -> (t0=((J[u,α+ϵ β]-J[u,α])/ϵ)),
2 -> (t1=(∫_0^1)(div[u, β//adSeries[((1-(E^(-s ad)))/ad), α]//RC[u, s α] // ad[u, α // RC[u,s α]]] // CC[u,-s α])\[DifferentialD]s),
3 -> (t2=(∫_0^1)(div[u, β//adSeries[((1-(E^(-s ad)))/ad), α]//RC[u, s α]] // ad[u, α // RC[u,s α]] // CC[u,-s α])\[DifferentialD]s),
4 -> (t3=(∫_0^1)(div[u, β//adSeries[(E^(-s ad)), α]// RC[u,s α]] // CC[u,-s α])\[DifferentialD]s),
t0 ≡ t1-t2+t3
};

Print /@ {
0 -> {α, β};
1 -> (t0=((J[u,α+ϵ β]-J[u,α])/ϵ)),
2 -> (t1=(∫_0^1)(div[u, β//Ad[-s α]// RC[u,s α]] // CC[u,-s α])\[DifferentialD]s),
3 -> (t2=(∫_0^1)(div[u, β//adSeries[((1-(E^(-s ad)))/ad), α]//RC[u, s α] // ad[u, α // RC[u,s α]]] // CC[u,-s α])\[DifferentialD]s),
4 -> (t3=(∫_0^1)(div[u, β//adSeries[((1-(E^(-s ad)))/ad), α]//RC[u, s α]] // ad[u, α // RC[u,s α]] // CC[u,-s α])\[DifferentialD]s),
t0 ≡ t1+t2-t3
};

Print /@ {
0 -> {α, β};
1 -> (t0=((J[u,α+ϵ β]-J[u,α])/ϵ)),
2 -> (t1=div[u, β//adSeries[((1-(E^(-ad)))/ad), α]//RC[u, α]] // CC[u,-α]),
t0 ≡ t1
};