In [1]:
using Flows

Check (1)


In [2]:
@t_vars t


Out[2]:
(t,)

In [3]:
@x_vars u,v


Out[3]:
(u,v)

In [4]:
@funs A, B


Out[4]:
(A,B)

In [5]:
E_Atu = E(A, t, u)


Out[5]:
$\mathcal{E}_{A}(t,u)$

In [6]:
E_Btv =E(B, t, v)


Out[6]:
$\mathcal{E}_{B}(t,v)$

In [7]:
Stu = E(B, t, E(A, t, u))


Out[7]:
$\mathcal{E}_{B}(t,\mathcal{E}_{A}(t,u))$

In [8]:
S1tv = differential(E(B,t,v), v, A(v)) -A(E(B,t,v))


Out[8]:
$-A(\mathcal{E}_{B}(t,v))+\partial_{2}\mathcal{E}_{B}(t,v)\cdot A(v)$

In [9]:
S1tu  = substitute(S1tv, v, E(A,t,u))
ex1 = S1tu


Out[9]:
$-A(\mathcal{E}_{B}(t,\mathcal{E}_{A}(t,u)))+\partial_{2}\mathcal{E}_{B}(t,\mathcal{E}_{A}(t,u))\cdot A(\mathcal{E}_{A}(t,u))$

In [10]:
ex2 = t_derivative(Stu, t) - (A(Stu) + B(Stu))


Out[10]:
$-A(\mathcal{E}_{B}(t,\mathcal{E}_{A}(t,u)))+\partial_{2}\mathcal{E}_{B}(t,\mathcal{E}_{A}(t,u))\cdot A(\mathcal{E}_{A}(t,u))$

In [11]:
ex1 - ex2


Out[11]:
$0$

Check (2)


In [12]:
ex1 = B(E(B,t,v), S1tv) + commutator(B,A,E(B,t,v))


Out[12]:
$B'(\mathcal{E}_{B}(t,v))\cdot (-A(\mathcal{E}_{B}(t,v))+\partial_{2}\mathcal{E}_{B}(t,v)\cdot A(v))+B'(\mathcal{E}_{B}(t,v))\cdot A(\mathcal{E}_{B}(t,v))-A'(\mathcal{E}_{B}(t,v))\cdot B(\mathcal{E}_{B}(t,v))$

In [13]:
ex2 = t_derivative(S1tv, t)


Out[13]:
$B'(\mathcal{E}_{B}(t,v))\cdot \partial_{2}\mathcal{E}_{B}(t,v)\cdot A(v)-A'(\mathcal{E}_{B}(t,v))\cdot B(\mathcal{E}_{B}(t,v))$

In [14]:
reduce_order(expand(ex1-ex2))


Out[14]:
$0$

Check (3)


In [15]:
@funs H


Out[15]:
(H,)

In [16]:
@nonautonomous_funs S


Out[16]:
(S,)

In [17]:
S1tu = t_derivative(S(t,u),t) - H(S(t,u))


Out[17]:
$\partial_{1}S(t,u)-H(S(t,u))$

In [18]:
S2tu = t_derivative(S1tu,t) - H(S(t,u),S1tu)


Out[18]:
$\partial_{1}^{2}S(t,u)-H'(S(t,u))\cdot (\partial_{1}S(t,u)-H(S(t,u)))-H'(S(t,u))\cdot \partial_{1}S(t,u)$

In [19]:
@t_vars T


Out[19]:
(T,)

In [20]:
ex1 = E(H,T-t,S(t,u),S2tu) + E(H,T-t,S(t,u),S1tu,S1tu)


Out[20]:
$\partial_{2}^{2}\mathcal{E}_{H}(T-t,S(t,u))(\partial_{1}S(t,u)-H(S(t,u)),\partial_{1}S(t,u)-H(S(t,u)))+\partial_{2}\mathcal{E}_{H}(T-t,S(t,u))\cdot (\partial_{1}^{2}S(t,u)-H'(S(t,u))\cdot (\partial_{1}S(t,u)-H(S(t,u)))-H'(S(t,u))\cdot \partial_{1}S(t,u))$

In [21]:
ex2 = t_derivative(E(H,T-t,S(t,u),S1tu),t)


Out[21]:
$\partial_{2}^{2}\mathcal{E}_{H}(T-t,S(t,u))(\partial_{1}S(t,u)-H(S(t,u)),\partial_{1}S(t,u))-H'(\mathcal{E}_{H}(T-t,S(t,u)))\cdot \partial_{2}\mathcal{E}_{H}(T-t,S(t,u))\cdot (\partial_{1}S(t,u)-H(S(t,u)))+\partial_{2}\mathcal{E}_{H}(T-t,S(t,u))\cdot (\partial_{1}^{2}S(t,u)-H'(S(t,u))\cdot \partial_{1}S(t,u))$

In [22]:
reduce_order(expand(ex1-ex2))


Out[22]:
$0$

Check(4)


In [23]:
S1tu  = substitute(S1tv, v, E(A,t,u))
S2tu = t_derivative(S1tu, t) - A(Stu, S1tu) - B(Stu, S1tu)
ex1 = S2tu


Out[23]:
$\partial_{2}\mathcal{E}_{B}(t,\mathcal{E}_{A}(t,u))\cdot A'(\mathcal{E}_{A}(t,u))\cdot A(\mathcal{E}_{A}(t,u))+\partial_{2}^{2}\mathcal{E}_{B}(t,\mathcal{E}_{A}(t,u))(A(\mathcal{E}_{A}(t,u)),A(\mathcal{E}_{A}(t,u)))+B'(\mathcal{E}_{B}(t,\mathcal{E}_{A}(t,u)))\cdot \partial_{2}\mathcal{E}_{B}(t,\mathcal{E}_{A}(t,u))\cdot A(\mathcal{E}_{A}(t,u))-A'(\mathcal{E}_{B}(t,\mathcal{E}_{A}(t,u)))\cdot (-A(\mathcal{E}_{B}(t,\mathcal{E}_{A}(t,u)))+\partial_{2}\mathcal{E}_{B}(t,\mathcal{E}_{A}(t,u))\cdot A(\mathcal{E}_{A}(t,u)))-B'(\mathcal{E}_{B}(t,\mathcal{E}_{A}(t,u)))\cdot (-A(\mathcal{E}_{B}(t,\mathcal{E}_{A}(t,u)))+\partial_{2}\mathcal{E}_{B}(t,\mathcal{E}_{A}(t,u))\cdot A(\mathcal{E}_{A}(t,u)))-A'(\mathcal{E}_{B}(t,\mathcal{E}_{A}(t,u)))\cdot (\partial_{2}\mathcal{E}_{B}(t,\mathcal{E}_{A}(t,u))\cdot A(\mathcal{E}_{A}(t,u))+B(\mathcal{E}_{B}(t,\mathcal{E}_{A}(t,u))))$

In [24]:
S2tv = differential(S1tv, v, A(v)) - A(E(B,t,v), S1tv) + commutator(B,A, E(B,t,v))
ex2 = substitute(S2tv, v, E(A,t,u))


Out[24]:
$\partial_{2}\mathcal{E}_{B}(t,\mathcal{E}_{A}(t,u))\cdot A'(\mathcal{E}_{A}(t,u))\cdot A(\mathcal{E}_{A}(t,u))+\partial_{2}^{2}\mathcal{E}_{B}(t,\mathcal{E}_{A}(t,u))(A(\mathcal{E}_{A}(t,u)),A(\mathcal{E}_{A}(t,u)))+B'(\mathcal{E}_{B}(t,\mathcal{E}_{A}(t,u)))\cdot A(\mathcal{E}_{B}(t,\mathcal{E}_{A}(t,u)))-A'(\mathcal{E}_{B}(t,\mathcal{E}_{A}(t,u)))\cdot (-A(\mathcal{E}_{B}(t,\mathcal{E}_{A}(t,u)))+\partial_{2}\mathcal{E}_{B}(t,\mathcal{E}_{A}(t,u))\cdot A(\mathcal{E}_{A}(t,u)))-A'(\mathcal{E}_{B}(t,\mathcal{E}_{A}(t,u)))\cdot B(\mathcal{E}_{B}(t,\mathcal{E}_{A}(t,u)))-A'(\mathcal{E}_{B}(t,\mathcal{E}_{A}(t,u)))\cdot \partial_{2}\mathcal{E}_{B}(t,\mathcal{E}_{A}(t,u))\cdot A(\mathcal{E}_{A}(t,u))$

In [25]:
expand(ex1 - ex2)


Out[25]:
$0$

Check (5)


In [26]:
@funs F, G, H 
substitute(substitute(commutator(F,G,v), G, commutator(G,H,v), v), v, u)


Out[26]:
$-G''(u)(H(u),F(u))-G'(u)\cdot H'(u)\cdot F(u)+H''(u)(G(u),F(u))+F'(u)\cdot (G'(u)\cdot H(u)-H'(u)\cdot G(u))+H'(u)\cdot G'(u)\cdot F(u)$

In [27]:
@x_vars w


Out[27]:
(w,)

In [28]:
ex1 = (B(E(B,t,v), S2tv) 
     +B(E(B,t,v), S1tv, S1tv)
     -commutator(B,B,A, E(B,t,v)) 
     -commutator(A,B,A, E(B,t,v)) 
     +2*substitute(differential(commutator(B,A,w), w, S1tv), w, E(B,t,v) ) )


Out[28]:
$B''(\mathcal{E}_{B}(t,v))(A(\mathcal{E}_{B}(t,v)),B(\mathcal{E}_{B}(t,v)))-2A''(\mathcal{E}_{B}(t,v))(B(\mathcal{E}_{B}(t,v)),-A(\mathcal{E}_{B}(t,v))+\partial_{2}\mathcal{E}_{B}(t,v)\cdot A(v))-A'(\mathcal{E}_{B}(t,v))\cdot (B'(\mathcal{E}_{B}(t,v))\cdot A(\mathcal{E}_{B}(t,v))-A'(\mathcal{E}_{B}(t,v))\cdot B(\mathcal{E}_{B}(t,v)))-A'(\mathcal{E}_{B}(t,v))\cdot B'(\mathcal{E}_{B}(t,v))\cdot A(\mathcal{E}_{B}(t,v))+B'(\mathcal{E}_{B}(t,v))\cdot (\partial_{2}^{2}\mathcal{E}_{B}(t,v)(A(v),A(v))-A'(\mathcal{E}_{B}(t,v))\cdot B(\mathcal{E}_{B}(t,v))-A'(\mathcal{E}_{B}(t,v))\cdot \partial_{2}\mathcal{E}_{B}(t,v)\cdot A(v)+\partial_{2}\mathcal{E}_{B}(t,v)\cdot A'(v)\cdot A(v)+B'(\mathcal{E}_{B}(t,v))\cdot A(\mathcal{E}_{B}(t,v))-A'(\mathcal{E}_{B}(t,v))\cdot (-A(\mathcal{E}_{B}(t,v))+\partial_{2}\mathcal{E}_{B}(t,v)\cdot A(v)))-A'(\mathcal{E}_{B}(t,v))\cdot B'(\mathcal{E}_{B}(t,v))\cdot B(\mathcal{E}_{B}(t,v))+B'(\mathcal{E}_{B}(t,v))\cdot A'(\mathcal{E}_{B}(t,v))\cdot B(\mathcal{E}_{B}(t,v))+B'(\mathcal{E}_{B}(t,v))\cdot A'(\mathcal{E}_{B}(t,v))\cdot A(\mathcal{E}_{B}(t,v))+B''(\mathcal{E}_{B}(t,v))(A(\mathcal{E}_{B}(t,v)),A(\mathcal{E}_{B}(t,v)))+2B'(\mathcal{E}_{B}(t,v))\cdot A'(\mathcal{E}_{B}(t,v))\cdot (-A(\mathcal{E}_{B}(t,v))+\partial_{2}\mathcal{E}_{B}(t,v)\cdot A(v))-A''(\mathcal{E}_{B}(t,v))(B(\mathcal{E}_{B}(t,v)),B(\mathcal{E}_{B}(t,v)))-2A'(\mathcal{E}_{B}(t,v))\cdot B'(\mathcal{E}_{B}(t,v))\cdot (-A(\mathcal{E}_{B}(t,v))+\partial_{2}\mathcal{E}_{B}(t,v)\cdot A(v))+B''(\mathcal{E}_{B}(t,v))(-A(\mathcal{E}_{B}(t,v))+\partial_{2}\mathcal{E}_{B}(t,v)\cdot A(v),-A(\mathcal{E}_{B}(t,v))+\partial_{2}\mathcal{E}_{B}(t,v)\cdot A(v))+2B''(\mathcal{E}_{B}(t,v))(A(\mathcal{E}_{B}(t,v)),-A(\mathcal{E}_{B}(t,v))+\partial_{2}\mathcal{E}_{B}(t,v)\cdot A(v))-A''(\mathcal{E}_{B}(t,v))(B(\mathcal{E}_{B}(t,v)),A(\mathcal{E}_{B}(t,v)))-B'(\mathcal{E}_{B}(t,v))\cdot (B'(\mathcal{E}_{B}(t,v))\cdot A(\mathcal{E}_{B}(t,v))-A'(\mathcal{E}_{B}(t,v))\cdot B(\mathcal{E}_{B}(t,v)))$

In [29]:
ex2 = t_derivative(S2tv, t)


Out[29]:
$B'(\mathcal{E}_{B}(t,v))\cdot \partial_{2}\mathcal{E}_{B}(t,v)\cdot A'(v)\cdot A(v)+B'(\mathcal{E}_{B}(t,v))\cdot \partial_{2}^{2}\mathcal{E}_{B}(t,v)(A(v),A(v))+B''(\mathcal{E}_{B}(t,v))(A(\mathcal{E}_{B}(t,v)),B(\mathcal{E}_{B}(t,v)))+B''(\mathcal{E}_{B}(t,v))(\partial_{2}\mathcal{E}_{B}(t,v)\cdot A(v),\partial_{2}\mathcal{E}_{B}(t,v)\cdot A(v))-A''(\mathcal{E}_{B}(t,v))(\partial_{2}\mathcal{E}_{B}(t,v)\cdot A(v),B(\mathcal{E}_{B}(t,v)))-A''(\mathcal{E}_{B}(t,v))(B(\mathcal{E}_{B}(t,v)),-A(\mathcal{E}_{B}(t,v))+\partial_{2}\mathcal{E}_{B}(t,v)\cdot A(v))-A'(\mathcal{E}_{B}(t,v))\cdot B'(\mathcal{E}_{B}(t,v))\cdot B(\mathcal{E}_{B}(t,v))+B'(\mathcal{E}_{B}(t,v))\cdot A'(\mathcal{E}_{B}(t,v))\cdot B(\mathcal{E}_{B}(t,v))-A''(\mathcal{E}_{B}(t,v))(B(\mathcal{E}_{B}(t,v)),B(\mathcal{E}_{B}(t,v)))-A'(\mathcal{E}_{B}(t,v))\cdot B'(\mathcal{E}_{B}(t,v))\cdot \partial_{2}\mathcal{E}_{B}(t,v)\cdot A(v)-A'(\mathcal{E}_{B}(t,v))\cdot (B'(\mathcal{E}_{B}(t,v))\cdot \partial_{2}\mathcal{E}_{B}(t,v)\cdot A(v)-A'(\mathcal{E}_{B}(t,v))\cdot B(\mathcal{E}_{B}(t,v)))$

In [30]:
expand(ex1-ex2)


Out[30]:
$0$

Check (6)


In [31]:
@t_vars T


Out[31]:
(T,)

In [32]:
@funs H


Out[32]:
(H,)

In [33]:
ex1 = t_derivative(E(H, T-t, Stu, E(B, t, E(A, t, u), commutator(B, A, E(A, t, u)))), t)


Out[33]:
$\partial_{2}\mathcal{E}_{H}(T-t,\mathcal{E}_{B}(t,\mathcal{E}_{A}(t,u)))\cdot (\partial_{2}^{2}\mathcal{E}_{B}(t,\mathcal{E}_{A}(t,u))(-A'(\mathcal{E}_{A}(t,u))\cdot B(\mathcal{E}_{A}(t,u))+B'(\mathcal{E}_{A}(t,u))\cdot A(\mathcal{E}_{A}(t,u)),A(\mathcal{E}_{A}(t,u)))+\partial_{2}\mathcal{E}_{B}(t,\mathcal{E}_{A}(t,u))\cdot (-A''(\mathcal{E}_{A}(t,u))(B(\mathcal{E}_{A}(t,u)),A(\mathcal{E}_{A}(t,u)))-A'(\mathcal{E}_{A}(t,u))\cdot B'(\mathcal{E}_{A}(t,u))\cdot A(\mathcal{E}_{A}(t,u))+B''(\mathcal{E}_{A}(t,u))(A(\mathcal{E}_{A}(t,u)),A(\mathcal{E}_{A}(t,u)))+B'(\mathcal{E}_{A}(t,u))\cdot A'(\mathcal{E}_{A}(t,u))\cdot A(\mathcal{E}_{A}(t,u)))+B'(\mathcal{E}_{B}(t,\mathcal{E}_{A}(t,u)))\cdot \partial_{2}\mathcal{E}_{B}(t,\mathcal{E}_{A}(t,u))\cdot (-A'(\mathcal{E}_{A}(t,u))\cdot B(\mathcal{E}_{A}(t,u))+B'(\mathcal{E}_{A}(t,u))\cdot A(\mathcal{E}_{A}(t,u))))-H'(\mathcal{E}_{H}(T-t,\mathcal{E}_{B}(t,\mathcal{E}_{A}(t,u))))\cdot \partial_{2}\mathcal{E}_{H}(T-t,\mathcal{E}_{B}(t,\mathcal{E}_{A}(t,u)))\cdot \partial_{2}\mathcal{E}_{B}(t,\mathcal{E}_{A}(t,u))\cdot (-A'(\mathcal{E}_{A}(t,u))\cdot B(\mathcal{E}_{A}(t,u))+B'(\mathcal{E}_{A}(t,u))\cdot A(\mathcal{E}_{A}(t,u)))+\partial_{2}^{2}\mathcal{E}_{H}(T-t,\mathcal{E}_{B}(t,\mathcal{E}_{A}(t,u)))(\partial_{2}\mathcal{E}_{B}(t,\mathcal{E}_{A}(t,u))\cdot (-A'(\mathcal{E}_{A}(t,u))\cdot B(\mathcal{E}_{A}(t,u))+B'(\mathcal{E}_{A}(t,u))\cdot A(\mathcal{E}_{A}(t,u))),\partial_{2}\mathcal{E}_{B}(t,\mathcal{E}_{A}(t,u))\cdot A(\mathcal{E}_{A}(t,u))+B(\mathcal{E}_{B}(t,\mathcal{E}_{A}(t,u))))$

In [34]:
ex2 = substitute(-E(H, T-t, E(B, t, v), E(B, t, v, commutator(A, B, A, v)))
                 +E(H, T-t, E(B, t, v), differential(S1tv, v, commutator(B, A, v)))
                 +E(H, T-t, E(B, t, v), S1tv, E(B, t, v, commutator(B, A, v)))
                ,v , E(A,t,u))


Out[34]:
$\partial_{2}^{2}\mathcal{E}_{H}(T-t,\mathcal{E}_{B}(t,\mathcal{E}_{A}(t,u)))(-A(\mathcal{E}_{B}(t,\mathcal{E}_{A}(t,u)))+\partial_{2}\mathcal{E}_{B}(t,\mathcal{E}_{A}(t,u))\cdot A(\mathcal{E}_{A}(t,u)),\partial_{2}\mathcal{E}_{B}(t,\mathcal{E}_{A}(t,u))\cdot (-A'(\mathcal{E}_{A}(t,u))\cdot B(\mathcal{E}_{A}(t,u))+B'(\mathcal{E}_{A}(t,u))\cdot A(\mathcal{E}_{A}(t,u))))-\partial_{2}\mathcal{E}_{H}(T-t,\mathcal{E}_{B}(t,\mathcal{E}_{A}(t,u)))\cdot \partial_{2}\mathcal{E}_{B}(t,\mathcal{E}_{A}(t,u))\cdot (A''(\mathcal{E}_{A}(t,u))(B(\mathcal{E}_{A}(t,u)),A(\mathcal{E}_{A}(t,u)))+A'(\mathcal{E}_{A}(t,u))\cdot B'(\mathcal{E}_{A}(t,u))\cdot A(\mathcal{E}_{A}(t,u))+A'(\mathcal{E}_{A}(t,u))\cdot (-A'(\mathcal{E}_{A}(t,u))\cdot B(\mathcal{E}_{A}(t,u))+B'(\mathcal{E}_{A}(t,u))\cdot A(\mathcal{E}_{A}(t,u)))-B''(\mathcal{E}_{A}(t,u))(A(\mathcal{E}_{A}(t,u)),A(\mathcal{E}_{A}(t,u)))-B'(\mathcal{E}_{A}(t,u))\cdot A'(\mathcal{E}_{A}(t,u))\cdot A(\mathcal{E}_{A}(t,u)))+\partial_{2}\mathcal{E}_{H}(T-t,\mathcal{E}_{B}(t,\mathcal{E}_{A}(t,u)))\cdot (\partial_{2}^{2}\mathcal{E}_{B}(t,\mathcal{E}_{A}(t,u))(-A'(\mathcal{E}_{A}(t,u))\cdot B(\mathcal{E}_{A}(t,u))+B'(\mathcal{E}_{A}(t,u))\cdot A(\mathcal{E}_{A}(t,u)),A(\mathcal{E}_{A}(t,u)))+\partial_{2}\mathcal{E}_{B}(t,\mathcal{E}_{A}(t,u))\cdot A'(\mathcal{E}_{A}(t,u))\cdot (-A'(\mathcal{E}_{A}(t,u))\cdot B(\mathcal{E}_{A}(t,u))+B'(\mathcal{E}_{A}(t,u))\cdot A(\mathcal{E}_{A}(t,u)))-A'(\mathcal{E}_{B}(t,\mathcal{E}_{A}(t,u)))\cdot \partial_{2}\mathcal{E}_{B}(t,\mathcal{E}_{A}(t,u))\cdot (-A'(\mathcal{E}_{A}(t,u))\cdot B(\mathcal{E}_{A}(t,u))+B'(\mathcal{E}_{A}(t,u))\cdot A(\mathcal{E}_{A}(t,u))))$

In [35]:
diff = ex1-ex2
diff = FE2DEF(ex1-ex2)
diff = substitute(diff, H, A(v)+B(v), v)
diff = 
expand(reduce_order(diff))


Out[35]:
$0$

In [ ]: