Pensieve header: Verifying the zipping theorem. Continues ZipBindDemo.nb in pensieve://Talks/Matemale-1804/.

HL[ℰ_] := Style[ℰ, Background -> Yellow];

Kδ/:(Subscript[Kδ, i_,j_]):=If[i===j,1,0];
{(SuperStar[z]),(SuperStar[x]),(SuperStar[y])}={ζ,ξ,η}; {(SuperStar[ζ]),(SuperStar[ξ]),(SuperStar[η])}={z,x,y};
(SuperStar[((Subscript[u_, i_]))]):=(Subscript[((SuperStar[u])), i]);

𝔼/:𝔼[Q1_,P1_]≡𝔼[Q2_,P2_]:=Simplify[Q1==Q2]∧Simplify[Normal[P1-P2]==0];

Zip

(Subscript[Zip, {}])[P_]:=P; (Subscript[Zip, {ζ_,ζs___}])[P_] := (Expand[P//(Subscript[Zip, {ζs}])] /. f_.(ζ^(d_.)):>(∂_({(SuperStar[ζ]),d}))f) /. (SuperStar[ζ])->0

(Subscript[Zip, {ζ}])[(a (ζ^6)+ζ+3)((z^5)(E^z)+7z)+99b]

(Subscript[Zip, {ξ,η}])[(ξ^3)(η^3)(E^(a x + b y+ c x y))]

(* 𝔼[Q,P] means (E^Q)P *)
𝔼 /: (Subscript[Zip, ζs_List])@𝔼[Q_,P_] := Module[{ζ,z,zs,c,ys,ηs,qt,zrule,Q1,Q2},
zs=Table[(SuperStar[ζ]),{ζ,ζs}];
c=Q/.Alternatives@@(ζs⋃zs)->0;
ys=Table[(∂_ζ)(Q/.Alternatives@@zs->0),{ζ,ζs}];
ηs=Table[(∂_z)(Q/.Alternatives@@ζs->0),{z,zs}];
qt=Inverse@Table[(Subscript[Kδ, z,(SuperStar[ζ])])-(∂_(z,ζ))Q,{ζ,ζs},{z,zs}];
zrule=Thread[zs->qt.(zs+ys)];
Q1=c+ηs.zs/.zrule;
Q2=Q1/.Alternatives@@zs->0;
Simplify /@ 𝔼[Q2,Det[qt](E^(-Q2))(Subscript[Zip, ζs])[(E^Q1)(P/.zrule)]] ];

Eh=𝔼[h(∑_(i=1)^3)(∑_(j=1)^3)(Subscript[a, 10i+j])(Subscript[x, i])(Subscript[ξ, j]),(∑_(i=1)^3)(Subscript[f, i])[(Subscript[x, 1]),(Subscript[x, 2]),(Subscript[x, 3])](Subscript[ξ, i])]; E1=Eh/.h->1

Short[lhs=(Subscript[Zip, {(Subscript[ξ, 1]),(Subscript[ξ, 2])}])@E1, 5]

HL[lhs==(Subscript[Zip, {(Subscript[ξ, 1])}])@(Subscript[Zip, {(Subscript[ξ, 2])}])@E1==(Subscript[Zip, {(Subscript[ξ, 2])}])@(Subscript[Zip, {(Subscript[ξ, 1])}])@E1]

Short[lhs=Normal[Eh /. 𝔼[Q_,P_] :> Series[P (E^Q),{h,0,3}]] // (Subscript[Zip, {(Subscript[ξ, 1]),(Subscript[ξ, 2])}]),5]

rhs=Normal[(Subscript[Zip, {(Subscript[ξ, 1]),(Subscript[ξ, 2])}])@Eh/. 𝔼[Q_,P_] :> Series[P (E^Q),{h,0,3}]];
HL@Simplify[lhs==rhs]

Zip2

𝔼 /: (Subscript[Zip2, ζs_List])@𝔼[Q_,P_] := Module[{ζ,z,zs,c,ys,ηs,qt,zrule,ζrule},
zs=Table[(SuperStar[ζ]),{ζ,ζs}];
c=Q/.Alternatives@@(ζs⋃zs)->0;
ys=Table[(∂_ζ)(Q/.Alternatives@@zs->0),{ζ,ζs}];
ηs=Table[(∂_z)(Q/.Alternatives@@ζs->0),{z,zs}];
qt=Inverse@Table[(Subscript[Kδ, z,(SuperStar[ζ])])-(∂_(z,ζ))Q,{ζ,ζs},{z,zs}];
zrule=Thread[zs->qt.(zs+ys)];
ζrule=Thread[ζs->ζs+ηs.qt];
Simplify /@ 𝔼[c+ηs.qt.ys,Det[qt](Subscript[Zip, ζs])[P/.(zrule⋃ζrule)]] ];

Short[(Subscript[Zip2, {(Subscript[ξ, 1]),(Subscript[ξ, 2])}])@E1, 5]

HL[(Subscript[Zip, {(Subscript[ξ, 1]),(Subscript[ξ, 2])}])@E1≡(Subscript[Zip2, {(Subscript[ξ, 1]),(Subscript[ξ, 2])}])@E1]

Eh2=𝔼[h(∑_(i=1)^3)(∑_(j=1)^3)(Subscript[a, 10i+j])(Subscript[x, i])(Subscript[ξ, j]),(∑_(i=1)^3)(∑_(j=1)^3)(Subscript[f, 10i+j])[(Subscript[x, 1]),(Subscript[x, 2]),(Subscript[x, 3])](Subscript[ξ, i])(Subscript[ξ, j])]; E2=Eh2/.h->1

Timing[lhs=(Subscript[Zip, {(Subscript[ξ, 1]),(Subscript[ξ, 2])}])@E2]

Timing[rhs=(Subscript[Zip2, {(Subscript[ξ, 1]),(Subscript[ξ, 2])}])@E2]

Timing@HL[lhs≡rhs]

Short[lhs=(Subscript[Zip2, {(Subscript[ξ, 1]),(Subscript[ξ, 2])}])@E1, 5]

HL[lhs==(Subscript[Zip2, {(Subscript[ξ, 1])}])@(Subscript[Zip2, {(Subscript[ξ, 2])}])@E1==(Subscript[Zip2, {(Subscript[ξ, 2])}])@(Subscript[Zip2, {(Subscript[ξ, 1])}])@E1]

Short[lhs=Normal[Eh /. 𝔼[Q_,P_] :> Series[P (E^Q),{h,0,3}]] // (Subscript[Zip, {(Subscript[ξ, 1]),(Subscript[ξ, 2])}]),5]

rhs=Normal[(Subscript[Zip2, {(Subscript[ξ, 1]),(Subscript[ξ, 2])}])@Eh/. 𝔼[Q_,P_] :> Series[P (E^Q),{h,0,3}]];
HL@Simplify[lhs==rhs]