

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