Cheat Sheet J - Verification

Pensieve header: Cheat Sheet Free Lie Verification; continues CheatSheetJ-Verification @ pensieve://2014-01/.

SetDirectory["C:\\drorbn\\AcademicPensieve\\Projects\\WKO4"];
<< FreeLie.m;

tm[u_,v_,w_] := LieMorphism[LW@u->LW@w, LW@v->LW@w];
ϵ /: (ϵ^2)=0;
Print /@ {{t,u,v,w} = LW /@ {"t","u","v","w"},
α = RandomLieSeries[{t,u,v}], δα = RandomLieSeries[{t,u,v}],
β = RandomLieSeries[{t,u,v}], δβ = RandomLieSeries[{t,u,v}],
γ = RandomLieSeries[{t,u,v}], δγ = RandomLieSeries[{t,u,v}]
};
$SeriesShowDegree=3; $SeriesCompareDegree = 6;

Some preliminary testing

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

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

The meaning(s) of RC

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

Print /@ {
1 -> α,
2 -> (t1= α // (Subscript[CC, u])[γ // (Subscript[RC, u])[γ]]),
3 -> (t2= α // (Subscript[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
};

The map Γ

Print /@ {
0 -> {λ=⟨u->α, v->β⟩,γ},
1 -> (t1= (Subscript[Γ, τ])[λ]),
2 -> (t2= γ  // DerivationExp[-τ (Subscript[D, λ])]),
3 -> (t3= γ // CC[(Subscript[Γ, τ])[λ]]),
4 -> t2≡t3
};

The map Λ

Print /@ {
0 -> {λ=⟨u->α, v->β⟩,γ},
1 -> (t1= (Subscript[Λ, τ])[λ]),
2 -> (t2= γ  // DerivationExp[-(Subscript[D, (Subscript[Λ, τ])[λ]])]),
3 -> (t3= γ // CC[τ λ]),
4 -> t2≡t3
};

Print /@ {
0 -> {λ=⟨u->α, v->β⟩},
1 -> (t1= (Subscript[Λ, τ])[λ]/τ),
2 -> (t2= (Subscript[Γ, τ])[t1]/τ),
4 -> 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 Definition of J

?J

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
};

The t equation

Print /@ {
0 -> γ,
1 -> (t1=(Subscript[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
};

The h equation

Print /@ {
1 -> (t1=(Subscript[J, u])[BCH[α, β]]),
2 -> (t2=(Subscript[J, u])[α]),
3 -> (t3=(Subscript[J, u])[β//(Subscript[RC, u])[α]]//(Subscript[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 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 C[⟨...⟩]

{λ=⟨u->α, v->β⟩, δλ=⟨u->δα, v->δβ⟩, γ}

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

The differential of RC

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

The differential of J

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