Theorem: SciLean.odeSolve.arg_x₀.revCDeriv_rule (SciLean/Modules/DifferentialEquations/OdeSolve.lean)

State before:
R✝ : Type ?u.22324
inst✝⁶ : RCLike R✝
X✝ : Type ?u.22330
inst✝⁵ : Vec R✝ X✝
R : Type u_1
inst✝⁴ : RCLike R
W : Type u_3
inst✝³ : SemiInnerProductSpace R W
X : Type u_2
inst✝² : SemiInnerProductSpace R X
Y : Type ?u.22376
inst✝¹ : SemiInnerProductSpace R Y
Z : Type ?u.22388
inst✝ : SemiInnerProductSpace R Z
f : R → X → X
t₀ t : R
x₀ : W → X
hf :
  HasAdjDiff R fun x =>
    match x with
    | (t, x) => f t x
hx : HasAdjDiff R x₀
⊢ <∂ w, odeSolve f t₀ t (x₀ w) = fun w =>
    let x₀dx₀ := <∂ x₀ w;
    let x := fun s => odeSolve f t₀ s x₀dx₀.1;
    let dfdx := fun s dx' => -∇ (x':=x s;dx'), f s x';
    (x t, fun dx =>
      let dx := odeSolve dfdx t₀ t dx;
      x₀dx₀.2 dx)
Tactic:
unfold gradient revDeriv
State after:
R✝ : Type ?u.22324
inst✝⁶ : RCLike R✝
X✝ : Type ?u.22330
inst✝⁵ : Vec R✝ X✝
R : Type u_1
inst✝⁴ : RCLike R
W : Type u_3
inst✝³ : SemiInnerProductSpace R W
X : Type u_2
inst✝² : SemiInnerProductSpace R X
Y : Type ?u.22376
inst✝¹ : SemiInnerProductSpace R Y
Z : Type ?u.22388
inst✝ : SemiInnerProductSpace R Z
f : R → X → X
t₀ t : R
x₀ : W → X
hf :
  HasAdjDiff R fun x =>
    match x with
    | (t, x) => f t x
hx : HasAdjDiff R x₀
⊢ (fun x => ((fun w => odeSolve f t₀ t (x₀ w)) x, semiAdjoint R (∂ (w:=x), odeSolve f t₀ t (x₀ w)))) = fun w =>
    let x₀dx₀ := (x₀ w, semiAdjoint R (∂ x₀ w));
    let x := fun s => odeSolve f t₀ s x₀dx₀.1;
    let dfdx := fun s dx' => -((fun x' => f s x') (x s), semiAdjoint R (∂ (x':=x s), f s x')).2 dx';
    (x t, fun dx =>
      let dx := odeSolve dfdx t₀ t dx;
      x₀dx₀.2 dx)

State before:
R✝ : Type ?u.22324
inst✝⁶ : RCLike R✝
X✝ : Type ?u.22330
inst✝⁵ : Vec R✝ X✝
R : Type u_1
inst✝⁴ : RCLike R
W : Type u_3
inst✝³ : SemiInnerProductSpace R W
X : Type u_2
inst✝² : SemiInnerProductSpace R X
Y : Type ?u.22376
inst✝¹ : SemiInnerProductSpace R Y
Z : Type ?u.22388
inst✝ : SemiInnerProductSpace R Z
f : R → X → X
t₀ t : R
x₀ : W → X
hf :
  HasAdjDiff R fun x =>
    match x with
    | (t, x) => f t x
hx : HasAdjDiff R x₀
⊢ (fun x => ((fun w => odeSolve f t₀ t (x₀ w)) x, semiAdjoint R (∂ (w:=x), odeSolve f t₀ t (x₀ w)))) = fun w =>
    let x₀dx₀ := (x₀ w, semiAdjoint R (∂ x₀ w));
    let x := fun s => odeSolve f t₀ s x₀dx₀.1;
    let dfdx := fun s dx' => -((fun x' => f s x') (x s), semiAdjoint R (∂ (x':=x s), f s x')).2 dx';
    (x t, fun dx =>
      let dx := odeSolve dfdx t₀ t dx;
      x₀dx₀.2 dx)
Tactic:
fun_trans
State after:
R✝ : Type ?u.22324
inst✝⁶ : RCLike R✝
X✝ : Type ?u.22330
inst✝⁵ : Vec R✝ X✝
R : Type u_1
inst✝⁴ : RCLike R
W : Type u_3
inst✝³ : SemiInnerProductSpace R W
X : Type u_2
inst✝² : SemiInnerProductSpace R X
Y : Type ?u.22376
inst✝¹ : SemiInnerProductSpace R Y
Z : Type ?u.22388
inst✝ : SemiInnerProductSpace R Z
f : R → X → X
t₀ t : R
x₀ : W → X
hf :
  HasAdjDiff R fun x =>
    match x with
    | (t, x) => f t x
hx : HasAdjDiff R x₀
⊢ (fun x =>
      (odeSolve f t₀ t (x₀ x),
        semiAdjoint R fun dw =>
          (odeSolve (fun t xdx => ∂> (wkx0wkx1:=(t, xdx.1);(0, xdx.2)), f wkx0wkx1.1 wkx0wkx1.2) t₀ t₀
              (∂> (w:=x;dw), x₀ w)).2)) =
    fun w =>
    (odeSolve f t₀ t (x₀ w), fun dx =>
      semiAdjoint R (∂ x₀ w)
        (odeSolve (fun s dx' => -semiAdjoint R (∂ (x':=odeSolve f t₀ s (x₀ w)), f s x') dx') t₀ t dx))

State before:
R✝ : Type ?u.22324
inst✝⁶ : RCLike R✝
X✝ : Type ?u.22330
inst✝⁵ : Vec R✝ X✝
R : Type u_1
inst✝⁴ : RCLike R
W : Type u_3
inst✝³ : SemiInnerProductSpace R W
X : Type u_2
inst✝² : SemiInnerProductSpace R X
Y : Type ?u.22376
inst✝¹ : SemiInnerProductSpace R Y
Z : Type ?u.22388
inst✝ : SemiInnerProductSpace R Z
f : R → X → X
t₀ t : R
x₀ : W → X
hf :
  HasAdjDiff R fun x =>
    match x with
    | (t, x) => f t x
hx : HasAdjDiff R x₀
⊢ (fun x =>
      (odeSolve f t₀ t (x₀ x),
        semiAdjoint R fun dw =>
          (odeSolve (fun t xdx => ∂> (wkx0wkx1:=(t, xdx.1);(0, xdx.2)), f wkx0wkx1.1 wkx0wkx1.2) t₀ t₀
              (∂> (w:=x;dw), x₀ w)).2)) =
    fun w =>
    (odeSolve f t₀ t (x₀ w), fun dx =>
      semiAdjoint R (∂ x₀ w)
        (odeSolve (fun s dx' => -semiAdjoint R (∂ (x':=odeSolve f t₀ s (x₀ w)), f s x') dx') t₀ t dx))
Tactic:
funext w
State after:
case h
R✝ : Type ?u.22324
inst✝⁶ : RCLike R✝
X✝ : Type ?u.22330
inst✝⁵ : Vec R✝ X✝
R : Type u_1
inst✝⁴ : RCLike R
W : Type u_3
inst✝³ : SemiInnerProductSpace R W
X : Type u_2
inst✝² : SemiInnerProductSpace R X
Y : Type ?u.22376
inst✝¹ : SemiInnerProductSpace R Y
Z : Type ?u.22388
inst✝ : SemiInnerProductSpace R Z
f : R → X → X
t₀ t : R
x₀ : W → X
hf :
  HasAdjDiff R fun x =>
    match x with
    | (t, x) => f t x
hx : HasAdjDiff R x₀
w : W
⊢ (odeSolve f t₀ t (x₀ w),
      semiAdjoint R fun dw =>
        (odeSolve (fun t xdx => ∂> (wkx0wkx1:=(t, xdx.1);(0, xdx.2)), f wkx0wkx1.1 wkx0wkx1.2) t₀ t₀
            (∂> (w:=w;dw), x₀ w)).2) =
    (odeSolve f t₀ t (x₀ w), fun dx =>
      semiAdjoint R (∂ x₀ w)
        (odeSolve (fun s dx' => -semiAdjoint R (∂ (x':=odeSolve f t₀ s (x₀ w)), f s x') dx') t₀ t dx))

State before:
case h
R✝ : Type ?u.22324
inst✝⁶ : RCLike R✝
X✝ : Type ?u.22330
inst✝⁵ : Vec R✝ X✝
R : Type u_1
inst✝⁴ : RCLike R
W : Type u_3
inst✝³ : SemiInnerProductSpace R W
X : Type u_2
inst✝² : SemiInnerProductSpace R X
Y : Type ?u.22376
inst✝¹ : SemiInnerProductSpace R Y
Z : Type ?u.22388
inst✝ : SemiInnerProductSpace R Z
f : R → X → X
t₀ t : R
x₀ : W → X
hf :
  HasAdjDiff R fun x =>
    match x with
    | (t, x) => f t x
hx : HasAdjDiff R x₀
w : W
⊢ (odeSolve f t₀ t (x₀ w),
      semiAdjoint R fun dw =>
        (odeSolve (fun t xdx => ∂> (wkx0wkx1:=(t, xdx.1);(0, xdx.2)), f wkx0wkx1.1 wkx0wkx1.2) t₀ t₀
            (∂> (w:=w;dw), x₀ w)).2) =
    (odeSolve f t₀ t (x₀ w), fun dx =>
      semiAdjoint R (∂ x₀ w)
        (odeSolve (fun s dx' => -semiAdjoint R (∂ (x':=odeSolve f t₀ s (x₀ w)), f s x') dx') t₀ t dx))
Tactic:
simp
State after:
case h
R✝ : Type ?u.22324
inst✝⁶ : RCLike R✝
X✝ : Type ?u.22330
inst✝⁵ : Vec R✝ X✝
R : Type u_1
inst✝⁴ : RCLike R
W : Type u_3
inst✝³ : SemiInnerProductSpace R W
X : Type u_2
inst✝² : SemiInnerProductSpace R X
Y : Type ?u.22376
inst✝¹ : SemiInnerProductSpace R Y
Z : Type ?u.22388
inst✝ : SemiInnerProductSpace R Z
f : R → X → X
t₀ t : R
x₀ : W → X
hf :
  HasAdjDiff R fun x =>
    match x with
    | (t, x) => f t x
hx : HasAdjDiff R x₀
w : W
⊢ (semiAdjoint R fun dw =>
      (odeSolve (fun t xdx => ∂> (wkx0wkx1:=(t, xdx.1);(0, xdx.2)), f wkx0wkx1.1 wkx0wkx1.2) t₀ t₀
          (∂> (w:=w;dw), x₀ w)).2) =
    fun dx =>
    semiAdjoint R (∂ x₀ w) (odeSolve (fun s dx' => -semiAdjoint R (∂ (x':=odeSolve f t₀ s (x₀ w)), f s x') dx') t₀ t dx)

State before:
case h
R✝ : Type ?u.22324
inst✝⁶ : RCLike R✝
X✝ : Type ?u.22330
inst✝⁵ : Vec R✝ X✝
R : Type u_1
inst✝⁴ : RCLike R
W : Type u_3
inst✝³ : SemiInnerProductSpace R W
X : Type u_2
inst✝² : SemiInnerProductSpace R X
Y : Type ?u.22376
inst✝¹ : SemiInnerProductSpace R Y
Z : Type ?u.22388
inst✝ : SemiInnerProductSpace R Z
f : R → X → X
t₀ t : R
x₀ : W → X
hf :
  HasAdjDiff R fun x =>
    match x with
    | (t, x) => f t x
hx : HasAdjDiff R x₀
w : W
⊢ (semiAdjoint R fun dw =>
      (odeSolve (fun t xdx => ∂> (wkx0wkx1:=(t, xdx.1);(0, xdx.2)), f wkx0wkx1.1 wkx0wkx1.2) t₀ t₀
          (∂> (w:=w;dw), x₀ w)).2) =
    fun dx =>
    semiAdjoint R (∂ x₀ w) (odeSolve (fun s dx' => -semiAdjoint R (∂ (x':=odeSolve f t₀ s (x₀ w)), f s x') dx') t₀ t dx)
Tactic:
sorry_proof
State after:
no goals