Theorem: SciLean.explicitSymplecticEuler_eq_implicitSymplecticEulerV1 (SciLean/Modules/DifferentialEquations/OdeSolvers/Solvers.lean)

State before:
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
⊢ (explicitSymplecticEuler fun q p => T p + V q) = implicitSymplecticEulerV1 fun q p => T p + V q
Tactic:
unfold implicitSymplecticEulerV1
State after:
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
⊢ (explicitSymplecticEuler fun q p => T p + V q) = fun Δt qₙ pₙ =>
    solve q' p',
      q' = qₙ + Δt • ∇ (p:=p'), (fun q p => T p + V q) qₙ p ∧ p' = pₙ - Δt • ∇ (q:=qₙ), (fun q p => T p + V q) q p'

State before:
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
⊢ (explicitSymplecticEuler fun q p => T p + V q) = fun Δt qₙ pₙ =>
    solve q' p',
      q' = qₙ + Δt • ∇ (p:=p'), (fun q p => T p + V q) qₙ p ∧ p' = pₙ - Δt • ∇ (q:=qₙ), (fun q p => T p + V q) q p'
Tactic:
unfold explicitSymplecticEuler
State after:
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ₙ pₙ =>
      let p' := pₙ - Δt • ∇ (q:=qₙ), (fun q p => T p + V q) q pₙ;
      let q' := qₙ + Δt • ∇ (p:=p'), (fun q p => T p + V q) qₙ p;
      (q', p')) =
    fun Δt qₙ pₙ =>
    solve q' p',
      q' = qₙ + Δt • ∇ (p:=p'), (fun q p => T p + V q) qₙ p ∧ p' = pₙ - Δt • ∇ (q:=qₙ), (fun q p => T p + V q) q p'

State before:
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ₙ pₙ =>
      let p' := pₙ - Δt • ∇ (q:=qₙ), (fun q p => T p + V q) q pₙ;
      let q' := qₙ + Δt • ∇ (p:=p'), (fun q p => T p + V q) qₙ p;
      (q', p')) =
    fun Δt qₙ pₙ =>
    solve q' p',
      q' = qₙ + Δt • ∇ (p:=p'), (fun q p => T p + V q) qₙ p ∧ p' = pₙ - Δt • ∇ (q:=qₙ), (fun q p => T p + V q) q p'
Tactic:
conv =>
  rhs
  solve_for p' from 1 := sorry_proof
  solve_as_inv
  solve_as_inv
State after:
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ₙ pₙ =>
      let p' := pₙ - Δt • ∇ (q:=qₙ), (fun q p => T p + V q) q pₙ;
      let q' := qₙ + Δt • ∇ (p:=p'), (fun q p => T p + V q) qₙ p;
      (q', p')) =
    fun Δt qₙ pₙ =>
    let p'' := fun q' => Function.invFun (fun x => x - (pₙ - Δt • ∇ (q:=qₙ), (T x + V q))) 0;
    let q' := Function.invFun (fun x => x - (qₙ + Δt • ∇ (p:=p'' x), (T p + V qₙ))) 0;
    let p' := p'' q';
    (q', p')

State before:
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ₙ pₙ =>
      let p' := pₙ - Δt • ∇ (q:=qₙ), (fun q p => T p + V q) q pₙ;
      let q' := qₙ + Δt • ∇ (p:=p'), (fun q p => T p + V q) qₙ p;
      (q', p')) =
    fun Δt qₙ pₙ =>
    let p'' := fun q' => Function.invFun (fun x => x - (pₙ - Δt • ∇ (q:=qₙ), (T x + V q))) 0;
    let q' := Function.invFun (fun x => x - (qₙ + Δt • ∇ (p:=p'' x), (T p + V qₙ))) 0;
    let p' := p'' q';
    (q', p')
Tactic:
autodiff
State after:
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')

State before:
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')
Tactic:
autodiff
State after:
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')

State before:
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')
Tactic:
sorry_proof
State after:
no goals