Theorem: SciLean.backwardEuler.isOdeStepper (SciLean/Modules/DifferentialEquations/OdeSolvers/BackwardEuler.lean)

State before:
R : Type u_1
inst✝³ : RCLike R
X : Type u_2
inst✝² : Vec R X
Y : Type ?u.676
inst✝¹ : Vec R Y
Z : Type ?u.688
inst✝ : Vec R Z
f : R → X → X
hf : CDifferentiable R fun tx => f tx.1 tx.2
hf' : ∀ (tₙ Δt : R), Diffeomorphism R fun x => x - Δt • f (tₙ + Δt) x
⊢ ∀ (t : R) (x : X), (Filter.limit (nhds 0) fun Δt' => ∂ (Δt:=Δt'), backwardEuler f t Δt x) = f t x
Tactic:
intro t x
State after:
R : Type u_1
inst✝³ : RCLike R
X : Type u_2
inst✝² : Vec R X
Y : Type ?u.676
inst✝¹ : Vec R Y
Z : Type ?u.688
inst✝ : Vec R Z
f : R → X → X
hf : CDifferentiable R fun tx => f tx.1 tx.2
hf' : ∀ (tₙ Δt : R), Diffeomorphism R fun x => x - Δt • f (tₙ + Δt) x
t : R
x : X
⊢ (Filter.limit (nhds 0) fun Δt' => ∂ (Δt:=Δt'), backwardEuler f t Δt x) = f t x

State before:
R : Type u_1
inst✝³ : RCLike R
X : Type u_2
inst✝² : Vec R X
Y : Type ?u.676
inst✝¹ : Vec R Y
Z : Type ?u.688
inst✝ : Vec R Z
f : R → X → X
hf : CDifferentiable R fun tx => f tx.1 tx.2
hf' : ∀ (tₙ Δt : R), Diffeomorphism R fun x => x - Δt • f (tₙ + Δt) x
t : R
x : X
⊢ (Filter.limit (nhds 0) fun Δt' => ∂ (Δt:=Δt'), backwardEuler f t Δt x) = f t x
Tactic:
unfold backwardEuler
State after:
R : Type u_1
inst✝³ : RCLike R
X : Type u_2
inst✝² : Vec R X
Y : Type ?u.676
inst✝¹ : Vec R Y
Z : Type ?u.688
inst✝ : Vec R Z
f : R → X → X
hf : CDifferentiable R fun tx => f tx.1 tx.2
hf' : ∀ (tₙ Δt : R), Diffeomorphism R fun x => x - Δt • f (tₙ + Δt) x
t : R
x : X
⊢ (Filter.limit (nhds 0) fun Δt' => ∂ (Δt:=Δt'), solve x', x' = x + Δt • f (t + Δt) x') = f t x

State before:
R : Type u_1
inst✝³ : RCLike R
X : Type u_2
inst✝² : Vec R X
Y : Type ?u.676
inst✝¹ : Vec R Y
Z : Type ?u.688
inst✝ : Vec R Z
f : R → X → X
hf : CDifferentiable R fun tx => f tx.1 tx.2
hf' : ∀ (tₙ Δt : R), Diffeomorphism R fun x => x - Δt • f (tₙ + Δt) x
t : R
x : X
⊢ (Filter.limit (nhds 0) fun Δt' => ∂ (Δt:=Δt'), solve x', x' = x + Δt • f (t + Δt) x') = f t x
Tactic:
conv =>
  conv in (solveFun _) =>
    conv in (_=_) =>
      move x' terms_to_lhs
  solve_as_inv
  autodiff
State after:
R : Type u_1
inst✝³ : RCLike R
X : Type u_2
inst✝² : Vec R X
Y : Type ?u.676
inst✝¹ : Vec R Y
Z : Type ?u.688
inst✝ : Vec R Z
f : R → X → X
hf : CDifferentiable R fun tx => f tx.1 tx.2
hf' : ∀ (tₙ Δt : R), Diffeomorphism R fun x => x - Δt • f (tₙ + Δt) x
t : R
x : X
⊢ (Filter.limit (nhds 0) fun Δt' =>
      let y := Function.invFun (fun x' => x' - Δt' • f (t + Δt') x') x;
      let y_1 := f (t + Δt') y;
      let y_2 := t + Δt';
      let dz := ∂ (x0:=y_2;1), f x0 y;
      let dfdx_y := -(Δt' • dz + y_1);
      let z := y - Δt' • f (t + Δt') y;
      let y := Function.invFun (fun x' => x' - Δt' • f (t + Δt') x') z;
      let dy := Function.invFun (fun dx => dx - Δt' • ∂ (x:=y;dx), f (t + Δt') x) dfdx_y;
      -dy) =
    f t x

State before:
R : Type u_1
inst✝³ : RCLike R
X : Type u_2
inst✝² : Vec R X
Y : Type ?u.676
inst✝¹ : Vec R Y
Z : Type ?u.688
inst✝ : Vec R Z
f : R → X → X
hf : CDifferentiable R fun tx => f tx.1 tx.2
hf' : ∀ (tₙ Δt : R), Diffeomorphism R fun x => x - Δt • f (tₙ + Δt) x
t : R
x : X
⊢ (Filter.limit (nhds 0) fun Δt' =>
      let y := Function.invFun (fun x' => x' - Δt' • f (t + Δt') x') x;
      let y_1 := f (t + Δt') y;
      let y_2 := t + Δt';
      let dz := ∂ (x0:=y_2;1), f x0 y;
      let dfdx_y := -(Δt' • dz + y_1);
      let z := y - Δt' • f (t + Δt') y;
      let y := Function.invFun (fun x' => x' - Δt' • f (t + Δt') x') z;
      let dy := Function.invFun (fun dx => dx - Δt' • ∂ (x:=y;dx), f (t + Δt') x) dfdx_y;
      -dy) =
    f t x
Tactic:
rw[Filter.limit_of_continuous _ _ sorry_proof]
State after:
R : Type u_1
inst✝³ : RCLike R
X : Type u_2
inst✝² : Vec R X
Y : Type ?u.676
inst✝¹ : Vec R Y
Z : Type ?u.688
inst✝ : Vec R Z
f : R → X → X
hf : CDifferentiable R fun tx => f tx.1 tx.2
hf' : ∀ (tₙ Δt : R), Diffeomorphism R fun x => x - Δt • f (tₙ + Δt) x
t : R
x : X
⊢ (let y := Function.invFun (fun x' => x' - 0 • f (t + 0) x') x;
    let y_1 := f (t + 0) y;
    let y_2 := t + 0;
    let dz := ∂ (x0:=y_2;1), f x0 y;
    let dfdx_y := -(0 • dz + y_1);
    let z := y - 0 • f (t + 0) y;
    let y := Function.invFun (fun x' => x' - 0 • f (t + 0) x') z;
    let dy := Function.invFun (fun dx => dx - 0 • ∂ (x:=y;dx), f (t + 0) x) dfdx_y;
    -dy) =
    f t x

State before:
R : Type u_1
inst✝³ : RCLike R
X : Type u_2
inst✝² : Vec R X
Y : Type ?u.676
inst✝¹ : Vec R Y
Z : Type ?u.688
inst✝ : Vec R Z
f : R → X → X
hf : CDifferentiable R fun tx => f tx.1 tx.2
hf' : ∀ (tₙ Δt : R), Diffeomorphism R fun x => x - Δt • f (tₙ + Δt) x
t : R
x : X
⊢ (let y := Function.invFun (fun x' => x' - 0 • f (t + 0) x') x;
    let y_1 := f (t + 0) y;
    let y_2 := t + 0;
    let dz := ∂ (x0:=y_2;1), f x0 y;
    let dfdx_y := -(0 • dz + y_1);
    let z := y - 0 • f (t + 0) y;
    let y := Function.invFun (fun x' => x' - 0 • f (t + 0) x') z;
    let dy := Function.invFun (fun dx => dx - 0 • ∂ (x:=y;dx), f (t + 0) x) dfdx_y;
    -dy) =
    f t x
Tactic:
fun_trans
State after:
no goals