autodiff
R : Type u_1
inst✝⁶ : RCLike R
X✝ : Type ?u.46671
inst✝⁵ : Vec R X✝
Y✝ : Type ?u.46685
inst✝⁴ : Vec R Y✝
Z✝ : Type ?u.46697
inst✝³ : Vec R Z✝
X : Type u_2
inst✝² : SemiInnerProductSpace R X
Y : Type ?u.46721
inst✝¹ : SemiInnerProductSpace R Y
Z : Type ?u.46733
inst✝ : SemiInnerProductSpace R Z
T V : X → R
hT : HasAdjDiff R T
hV : HasAdjDiff R V
⊢ (fun Δt qₙ =>
      let ydg := <∂ (q:=qₙ), V q;
      fun pₙ =>
      let zdf := <∂ (q5:=ydg.1), (T pₙ + q5);
      let dy := zdf.2 1;
      let p' := pₙ - Δt • ydg.2 dy;
      let ydg := <∂ (p:=p'), T p;
      let zdf := <∂ (p4:=ydg.1), (p4 + V qₙ);
      let dy := zdf.2 1;
      let q' := qₙ + Δt • ydg.2 dy;
      (q', p')) =
    fun Δt qₙ =>
    let ydg := <∂ (q:=qₙ), V q;
    fun pₙ =>
    let ydg_1 :=
      <∂
        (p:=Function.invFun
          (fun x =>
            let zdf := <∂ (q5:=ydg.1), (T x + q5);
            let dy := zdf.2 1;
            x - (pₙ - Δt • ydg.2 dy))
          0),
        T p;
    let zdf := <∂ (p4:=ydg_1.1), (p4 + V qₙ);
    let dy := zdf.2 1;
    let q' := Function.invFun (fun x => x - (qₙ + Δt • ydg_1.2 dy)) 0;
    let p' :=
      Function.invFun
        (fun x =>
          let zdf := <∂ (q5:=ydg.1), (T x + q5);
          let dy := zdf.2 1;
          x - (pₙ - Δt • ydg.2 dy))
        0;
    (q', p')
R : Type u_1
inst✝⁶ : RCLike R
X✝ : Type ?u.46671
inst✝⁵ : Vec R X✝
Y✝ : Type ?u.46685
inst✝⁴ : Vec R Y✝
Z✝ : Type ?u.46697
inst✝³ : Vec R Z✝
X : Type u_2
inst✝² : SemiInnerProductSpace R X
Y : Type ?u.46721
inst✝¹ : SemiInnerProductSpace R Y
Z : Type ?u.46733
inst✝ : SemiInnerProductSpace R Z
T V : X → R
hT : HasAdjDiff R T
hV : HasAdjDiff R V
⊢ (fun Δt qₙ =>
      let ydg := <∂ (q:=qₙ), V q;
      fun pₙ =>
      let zdf := <∂ (q5:=ydg.1), (T pₙ + q5);
      let dy := zdf.2 1;
      let p' := pₙ - Δt • ydg.2 dy;
      let ydg := <∂ (p:=p'), T p;
      let zdf := <∂ (p4:=ydg.1), (p4 + V qₙ);
      let dy := zdf.2 1;
      let q' := qₙ + Δt • ydg.2 dy;
      (q', p')) =
    fun Δt qₙ =>
    let ydg := <∂ (q:=qₙ), V q;
    fun pₙ =>
    let ydg_1 :=
      <∂
        (p:=Function.invFun
          (fun x =>
            let zdf := <∂ (q5:=ydg.1), (T x + q5);
            let dy := zdf.2 1;
            x - (pₙ - Δt • ydg.2 dy))
          0),
        T p;
    let zdf := <∂ (p4:=ydg_1.1), (p4 + V qₙ);
    let dy := zdf.2 1;
    let q' := qₙ + Δt • ydg_1.2 dy;
    let p' :=
      Function.invFun
        (fun x =>
          let zdf := <∂ (q5:=ydg.1), (T x + q5);
          let dy := zdf.2 1;
          x - (pₙ - Δt • ydg.2 dy))
        0;
    (q', p')