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 [ ]: