internlm/Lean-Github huggingface dataset:
Theorem: SciLean.parDistribFwdDeriv.bind_rule
Proof state before:
R : Type u_1
inst✝⁸ : RealScalar R
W : Type u_6
inst✝⁷ : Vec R W
X : Type u_7
inst✝⁶ : Vec R X
Y : Type u_4
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type u_2
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type u_5
inst✝¹ : Vec R U
V : Type u_3
inst✝ : Vec R V
f : X → Y → 𝒟'(Z, V)
g : X → 𝒟'(Y, U)
L : U ⊸[R] V ⊸[R] W
hf :
  DistribDifferentiable fun x =>
    match x with
    | (x, y) => f x y
hg : DistribDifferentiable g
⊢ (parDistribFwdDeriv fun x => Distribution.bind (g x) (f x) L) = fun x dx =>
    let ydy := parDistribFwdDeriv g x dx;
    let zdz := fun y => parDistribFwdDeriv (fun x => f x y) x dx;
    Distribution.bind ydy zdz
      (fun x ⊸[R]
        match x with
        | (r, dr) =>
          fun x ⊸[R]
            match x with
            | (s, ds) => ((L r) s, (L r) ds + (L dr) s))
Tactic:
unfold parDistribFwdDeriv Distribution.bind
Proof state after:
R : Type u_1
inst✝⁸ : RealScalar R
W : Type u_6
inst✝⁷ : Vec R W
X : Type u_7
inst✝⁶ : Vec R X
Y : Type u_4
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type u_2
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type u_5
inst✝¹ : Vec R U
V : Type u_3
inst✝ : Vec R V
f : X → Y → 𝒟'(Z, V)
g : X → 𝒟'(Y, U)
L : U ⊸[R] V ⊸[R] W
hf :
  DistribDifferentiable fun x =>
    match x with
    | (x, y) => f x y
hg : DistribDifferentiable g
⊢ (fun x dx =>
      let dz :=
        postComp
          (parDistribDeriv (fun x => fun φ ⊸[R] ⟪g x, fun x_1 => ⟪f x x_1, ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v]⟫[L]) x dx)
          (fun dz ⊸[R] (0, dz));
      let z :=
        postComp ((fun x => fun φ ⊸[R] ⟪g x, fun x_1 => ⟪f x x_1, ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v]⟫[L]) x)
          (fun z ⊸[R] (z, 0));
      z + dz) =
    fun x dx =>
    let ydy :=
      let dz := postComp (parDistribDeriv g x dx) (fun dz ⊸[R] (0, dz));
      let z := postComp (g x) (fun z ⊸[R] (z, 0));
      z + dz;
    let zdz := fun y =>
      let dz := postComp (parDistribDeriv (fun x => f x y) x dx) (fun dz ⊸[R] (0, dz));
      let z := postComp ((fun x => f x y) x) (fun z ⊸[R] (z, 0));
      z + dz;
    fun φ ⊸[R]
      ⟪ydy, fun x =>
        ⟪zdz x, ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v]⟫[fun x ⊸[R]
          match x with
          | (r, dr) =>
            fun x ⊸[R]
              match x with
              | (s, ds) => ((L r) s, (L r) ds + (L dr) s)]
Theorem: SciLean.parDistribFwdDeriv.bind_rule
Proof state before:
R : Type u_1
inst✝⁸ : RealScalar R
W : Type u_6
inst✝⁷ : Vec R W
X : Type u_7
inst✝⁶ : Vec R X
Y : Type u_4
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type u_2
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type u_5
inst✝¹ : Vec R U
V : Type u_3
inst✝ : Vec R V
f : X → Y → 𝒟'(Z, V)
g : X → 𝒟'(Y, U)
L : U ⊸[R] V ⊸[R] W
hf :
  DistribDifferentiable fun x =>
    match x with
    | (x, y) => f x y
hg : DistribDifferentiable g
⊢ (fun x dx =>
      let dz :=
        postComp
          (parDistribDeriv (fun x => fun φ ⊸[R] ⟪g x, fun x_1 => ⟪f x x_1, ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v]⟫[L]) x dx)
          (fun dz ⊸[R] (0, dz));
      let z :=
        postComp ((fun x => fun φ ⊸[R] ⟪g x, fun x_1 => ⟪f x x_1, ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v]⟫[L]) x)
          (fun z ⊸[R] (z, 0));
      z + dz) =
    fun x dx =>
    let ydy :=
      let dz := postComp (parDistribDeriv g x dx) (fun dz ⊸[R] (0, dz));
      let z := postComp (g x) (fun z ⊸[R] (z, 0));
      z + dz;
    let zdz := fun y =>
      let dz := postComp (parDistribDeriv (fun x => f x y) x dx) (fun dz ⊸[R] (0, dz));
      let z := postComp ((fun x => f x y) x) (fun z ⊸[R] (z, 0));
      z + dz;
    fun φ ⊸[R]
      ⟪ydy, fun x =>
        ⟪zdz x, ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v]⟫[fun x ⊸[R]
          match x with
          | (r, dr) =>
            fun x ⊸[R]
              match x with
              | (s, ds) => ((L r) s, (L r) ds + (L dr) s)]
Tactic:
autodiff
Proof state after:
R : Type u_1
inst✝⁸ : RealScalar R
W : Type u_6
inst✝⁷ : Vec R W
X : Type u_7
inst✝⁶ : Vec R X
Y : Type u_4
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type u_2
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type u_5
inst✝¹ : Vec R U
V : Type u_3
inst✝ : Vec R V
f : X → Y → 𝒟'(Z, V)
g : X → 𝒟'(Y, U)
L : U ⊸[R] V ⊸[R] W
hf :
  DistribDifferentiable fun x =>
    match x with
    | (x, y) => f x y
hg : DistribDifferentiable g
⊢ (fun x =>
      let z :=
        postComp (fun φ ⊸[R] ⟪g x, fun x_1 => ⟪f x x_1, ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v]⟫[L]) (fun z ⊸[R] (z, 0));
      fun dx =>
      let dz :=
        postComp
          (parDistribDeriv (fun x => fun φ ⊸[R] ⟪g x, fun x_1 => ⟪f x x_1, ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v]⟫[L]) x dx)
          (fun dz ⊸[R] (0, dz));
      z + dz) =
    fun x =>
    let z := postComp (g x) (fun z ⊸[R] (z, 0));
    fun dx =>
    let dz := postComp (parDistribDeriv g x dx) (fun dz ⊸[R] (0, dz));
    let ydy := z + dz;
    fun φ ⊸[R]
      ⟪ydy, fun x_1 =>
        let dz := postComp (parDistribDeriv (fun x => f x x_1) x dx) (fun dz ⊸[R] (0, dz));
        let z := postComp (f x x_1) (fun z ⊸[R] (z, 0));
        ⟪z + dz,
          ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v]⟫[fun x ⊸[R] fun x_1 ⊸[R] ((L x.1) x_1.1, (L x.1) x_1.2 + (L x.2) x_1.1)]
Theorem: SciLean.parDistribFwdDeriv.bind_rule
Proof state before:
R : Type u_1
inst✝⁸ : RealScalar R
W : Type u_6
inst✝⁷ : Vec R W
X : Type u_7
inst✝⁶ : Vec R X
Y : Type u_4
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type u_2
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type u_5
inst✝¹ : Vec R U
V : Type u_3
inst✝ : Vec R V
f : X → Y → 𝒟'(Z, V)
g : X → 𝒟'(Y, U)
L : U ⊸[R] V ⊸[R] W
hf :
  DistribDifferentiable fun x =>
    match x with
    | (x, y) => f x y
hg : DistribDifferentiable g
⊢ (fun x =>
      let z :=
        postComp (fun φ ⊸[R] ⟪g x, fun x_1 => ⟪f x x_1, ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v]⟫[L]) (fun z ⊸[R] (z, 0));
      fun dx =>
      let dz :=
        postComp
          (parDistribDeriv (fun x => fun φ ⊸[R] ⟪g x, fun x_1 => ⟪f x x_1, ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v]⟫[L]) x dx)
          (fun dz ⊸[R] (0, dz));
      z + dz) =
    fun x =>
    let z := postComp (g x) (fun z ⊸[R] (z, 0));
    fun dx =>
    let dz := postComp (parDistribDeriv g x dx) (fun dz ⊸[R] (0, dz));
    let ydy := z + dz;
    fun φ ⊸[R]
      ⟪ydy, fun x_1 =>
        let dz := postComp (parDistribDeriv (fun x => f x x_1) x dx) (fun dz ⊸[R] (0, dz));
        let z := postComp (f x x_1) (fun z ⊸[R] (z, 0));
        ⟪z + dz,
          ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v]⟫[fun x ⊸[R] fun x_1 ⊸[R] ((L x.1) x_1.1, (L x.1) x_1.2 + (L x.2) x_1.1)]
Tactic:
funext x dx
Proof state after:
case h.h
R : Type u_1
inst✝⁸ : RealScalar R
W : Type u_6
inst✝⁷ : Vec R W
X : Type u_7
inst✝⁶ : Vec R X
Y : Type u_4
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type u_2
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type u_5
inst✝¹ : Vec R U
V : Type u_3
inst✝ : Vec R V
f : X → Y → 𝒟'(Z, V)
g : X → 𝒟'(Y, U)
L : U ⊸[R] V ⊸[R] W
hf :
  DistribDifferentiable fun x =>
    match x with
    | (x, y) => f x y
hg : DistribDifferentiable g
x dx : X
⊢ (let z := postComp (fun φ ⊸[R] ⟪g x, fun x_1 => ⟪f x x_1, ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v]⟫[L]) (fun z ⊸[R] (z, 0));
      fun dx =>
      let dz :=
        postComp
          (parDistribDeriv (fun x => fun φ ⊸[R] ⟪g x, fun x_1 => ⟪f x x_1, ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v]⟫[L]) x dx)
          (fun dz ⊸[R] (0, dz));
      z + dz)
      dx =
    (let z := postComp (g x) (fun z ⊸[R] (z, 0));
      fun dx =>
      let dz := postComp (parDistribDeriv g x dx) (fun dz ⊸[R] (0, dz));
      let ydy := z + dz;
      fun φ ⊸[R]
        ⟪ydy, fun x_1 =>
          let dz := postComp (parDistribDeriv (fun x => f x x_1) x dx) (fun dz ⊸[R] (0, dz));
          let z := postComp (f x x_1) (fun z ⊸[R] (z, 0));
          ⟪z + dz,
            ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v]⟫[fun x ⊸[R] fun x_1 ⊸[R] ((L x.1) x_1.1, (L x.1) x_1.2 + (L x.2) x_1.1)])
      dx
Theorem: SciLean.parDistribFwdDeriv.bind_rule
Proof state before:
case h.h
R : Type u_1
inst✝⁸ : RealScalar R
W : Type u_6
inst✝⁷ : Vec R W
X : Type u_7
inst✝⁶ : Vec R X
Y : Type u_4
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type u_2
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type u_5
inst✝¹ : Vec R U
V : Type u_3
inst✝ : Vec R V
f : X → Y → 𝒟'(Z, V)
g : X → 𝒟'(Y, U)
L : U ⊸[R] V ⊸[R] W
hf :
  DistribDifferentiable fun x =>
    match x with
    | (x, y) => f x y
hg : DistribDifferentiable g
x dx : X
⊢ (let z := postComp (fun φ ⊸[R] ⟪g x, fun x_1 => ⟪f x x_1, ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v]⟫[L]) (fun z ⊸[R] (z, 0));
      fun dx =>
      let dz :=
        postComp
          (parDistribDeriv (fun x => fun φ ⊸[R] ⟪g x, fun x_1 => ⟪f x x_1, ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v]⟫[L]) x dx)
          (fun dz ⊸[R] (0, dz));
      z + dz)
      dx =
    (let z := postComp (g x) (fun z ⊸[R] (z, 0));
      fun dx =>
      let dz := postComp (parDistribDeriv g x dx) (fun dz ⊸[R] (0, dz));
      let ydy := z + dz;
      fun φ ⊸[R]
        ⟪ydy, fun x_1 =>
          let dz := postComp (parDistribDeriv (fun x => f x x_1) x dx) (fun dz ⊸[R] (0, dz));
          let z := postComp (f x x_1) (fun z ⊸[R] (z, 0));
          ⟪z + dz,
            ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v]⟫[fun x ⊸[R] fun x_1 ⊸[R] ((L x.1) x_1.1, (L x.1) x_1.2 + (L x.2) x_1.1)])
      dx
Tactic:
fun_trans [action_push,fwdDeriv]
Proof state after:
case h.h
R : Type u_1
inst✝⁸ : RealScalar R
W : Type u_6
inst✝⁷ : Vec R W
X : Type u_7
inst✝⁶ : Vec R X
Y : Type u_4
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type u_2
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type u_5
inst✝¹ : Vec R U
V : Type u_3
inst✝ : Vec R V
f : X → Y → 𝒟'(Z, V)
g : X → 𝒟'(Y, U)
L : U ⊸[R] V ⊸[R] W
hf :
  DistribDifferentiable fun x =>
    match x with
    | (x, y) => f x y
hg : DistribDifferentiable g
x dx : X
⊢ postComp (fun φ ⊸[R] ⟪g x, fun x_1 => ⟪f x x_1, ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v]⟫[L]) (fun z ⊸[R] (z, 0)) +
      postComp
        (parDistribDeriv (fun x => fun φ ⊸[R] ⟪g x, fun x_1 => ⟪f x x_1, ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v]⟫[L]) x dx)
        (fun dz ⊸[R] (0, dz)) =
    fun φ ⊸[R]
      ⟪postComp (g x) (fun z ⊸[R] (z, 0)), fun x_1 =>
          ⟪postComp (f x x_1) (fun z ⊸[R] (z, 0)), ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v] +
            ⟪postComp (parDistribDeriv (fun x => f x x_1) x dx) (fun dz ⊸[R] (0, dz)),
              ⇑φ⟫[fun v ⊸[R]
                fun r ⊸[R] r • v]⟫[fun x ⊸[R] fun x_1 ⊸[R] ((L x.1) x_1.1, (L x.1) x_1.2 + (L x.2) x_1.1)] +
        ⟪postComp (parDistribDeriv g x dx) (fun dz ⊸[R] (0, dz)), fun x_1 =>
          ⟪postComp (f x x_1) (fun z ⊸[R] (z, 0)), ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v] +
            ⟪postComp (parDistribDeriv (fun x => f x x_1) x dx) (fun dz ⊸[R] (0, dz)),
              ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v]⟫[fun x ⊸[R] fun x_1 ⊸[R] ((L x.1) x_1.1, (L x.1) x_1.2 + (L x.2) x_1.1)]
Theorem: SciLean.parDistribFwdDeriv.bind_rule
Proof state before:
case h.h.a.a
R : Type u_1
inst✝⁸ : RealScalar R
W : Type u_6
inst✝⁷ : Vec R W
X : Type u_7
inst✝⁶ : Vec R X
Y : Type u_4
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type u_2
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type u_5
inst✝¹ : Vec R U
V : Type u_3
inst✝ : Vec R V
f : X → Y → 𝒟'(Z, V)
g : X → 𝒟'(Y, U)
L : U ⊸[R] V ⊸[R] W
hf :
  DistribDifferentiable fun x =>
    match x with
    | (x, y) => f x y
hg : DistribDifferentiable g
x dx : X
φ : 𝒟 Z
⊢ ((postComp (fun φ ⊸[R] ⟪g x, fun x_1 => ⟪f x x_1, ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v]⟫[L]) (fun z ⊸[R] (z, 0)) +
          postComp
            (parDistribDeriv (fun x => fun φ ⊸[R] ⟪g x, fun x_1 => ⟪f x x_1, ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v]⟫[L]) x dx)
            (fun dz ⊸[R] (0, dz)))
        φ).2 =
    ((fun φ ⊸[R]
          ⟪postComp (g x) (fun z ⊸[R] (z, 0)), fun x_1 =>
              ⟪postComp (f x x_1) (fun z ⊸[R] (z, 0)), ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v] +
                ⟪postComp (parDistribDeriv (fun x => f x x_1) x dx) (fun dz ⊸[R] (0, dz)),
                  ⇑φ⟫[fun v ⊸[R]
                    fun r ⊸[R] r • v]⟫[fun x ⊸[R] fun x_1 ⊸[R] ((L x.1) x_1.1, (L x.1) x_1.2 + (L x.2) x_1.1)] +
            ⟪postComp (parDistribDeriv g x dx) (fun dz ⊸[R] (0, dz)), fun x_1 =>
              ⟪postComp (f x x_1) (fun z ⊸[R] (z, 0)), ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v] +
                ⟪postComp (parDistribDeriv (fun x => f x x_1) x dx) (fun dz ⊸[R] (0, dz)),
                  ⇑φ⟫[fun v ⊸[R]
                    fun r ⊸[R] r • v]⟫[fun x ⊸[R] fun x_1 ⊸[R] ((L x.1) x_1.1, (L x.1) x_1.2 + (L x.2) x_1.1)])
        φ).2
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.backwardEuler.isOdeStepper
Proof 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
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
⊢ (Filter.limit (nhds 0) fun Δt' => ∂ (Δt:=Δt'), backwardEuler f t Δt x) = f t x
Theorem: SciLean.backwardEuler.isOdeStepper
Proof 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
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
⊢ (Filter.limit (nhds 0) fun Δt' => ∂ (Δt:=Δt'), solve x', x' = x + Δt • f (t + Δt) x') = f t x
Theorem: SciLean.backwardEuler.isOdeStepper
Proof 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
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
⊢ (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
Theorem: SciLean.backwardEuler.isOdeStepper
Proof 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]
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
Theorem: SciLean.backwardEuler.isOdeStepper
Proof 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
Proof state after:
no goals
Theorem: SciLean.StructType.structProj_structMake
Proof state before:
X : Sort u_2
I : Sort u_3
XI : I → Sort u_1
inst✝ : StructType X I XI
f : (i : I) → XI i
i : I
⊢ structProj (structMake f) i = f i
Tactic:
apply congr_fun
Proof state after:
case h
X : Sort u_2
I : Sort u_3
XI : I → Sort u_1
inst✝ : StructType X I XI
f : (i : I) → XI i
i : I
⊢ structProj (structMake f) = fun i => f i
Theorem: SciLean.StructType.structProj_structMake
Proof state before:
case h
X : Sort u_2
I : Sort u_3
XI : I → Sort u_1
inst✝ : StructType X I XI
f : (i : I) → XI i
i : I
⊢ structProj (structMake f) = fun i => f i
Tactic:
apply left_inv
Proof state after:
no goals
Theorem: SciLean.StructType.structMake_structProj
Proof state before:
X : Sort u_1
I : Sort u_2
XI : I → Sort u_3
inst✝ : StructType X I XI
x : X
⊢ (structMake fun i => structProj x i) = x
Tactic:
apply right_inv
Proof state after:
no goals
Theorem: SciLean.StructType.structProj_oneHot
Proof state before:
X : Sort u_3
I : Sort u_1
XI : I → Type u_2
inst✝² : StructType X I XI
i : I
inst✝¹ : DecidableEq I
inst✝ : (i : I) → Zero (XI i)
xi : XI i
⊢ structProj (oneHot i xi) i = xi
Tactic:
simp[oneHot]
Proof state after:
no goals
Theorem: SciLean.StructType.structProj_oneHot'
Proof state before:
X : Sort u_3
I : Sort u_1
XI : I → Type u_2
inst✝² : StructType X I XI
inst✝¹ : DecidableEq I
inst✝ : (i : I) → Zero (XI i)
i j : I
xi : XI i
h : i ≠ j
⊢ structProj (oneHot i xi) j = 0
Tactic:
simp[oneHot]
Proof state after:
X : Sort u_3
I : Sort u_1
XI : I → Type u_2
inst✝² : StructType X I XI
inst✝¹ : DecidableEq I
inst✝ : (i : I) → Zero (XI i)
i j : I
xi : XI i
h : i ≠ j
⊢ ∀ (h : i = j), h ▸ xi = 0
Theorem: SciLean.StructType.structProj_oneHot'
Proof state before:
X : Sort u_3
I : Sort u_1
XI : I → Type u_2
inst✝² : StructType X I XI
inst✝¹ : DecidableEq I
inst✝ : (i : I) → Zero (XI i)
i j : I
xi : XI i
h : i ≠ j
⊢ ∀ (h : i = j), h ▸ xi = 0
Tactic:
if h':i=j then simp [h'] at h else simp[h']
Proof state after:
no goals
Theorem: SciLean.StructType.structProj_oneHot'
Proof state before:
X : Sort u_3
I : Sort u_1
XI : I → Type u_2
inst✝² : StructType X I XI
inst✝¹ : DecidableEq I
inst✝ : (i : I) → Zero (XI i)
i j : I
xi : XI i
h : i ≠ j
h' : i = j
⊢ ∀ (h : i = j), h ▸ xi = 0
Tactic:
simp [h'] at h
Proof state after:
no goals
Theorem: SciLean.StructType.structProj_oneHot'
Proof state before:
X : Sort u_3
I : Sort u_1
XI : I → Type u_2
inst✝² : StructType X I XI
inst✝¹ : DecidableEq I
inst✝ : (i : I) → Zero (XI i)
i j : I
xi : XI i
h : i ≠ j
h' : ¬i = j
⊢ ∀ (h : i = j), h ▸ xi = 0
Tactic:
simp[h']
Proof state after:
no goals
Theorem: SciLean.structExt
Proof state before:
X : Sort u_2
I : Sort u_3
XI : I → Sort u_1
inst✝ : StructType X I XI
x x' : X
⊢ (∀ (i : I), structProj x i = structProj x' i) → x = x'
Tactic:
intro h
Proof state after:
X : Sort u_2
I : Sort u_3
XI : I → Sort u_1
inst✝ : StructType X I XI
x x' : X
h : ∀ (i : I), structProj x i = structProj x' i
⊢ x = x'
Theorem: SciLean.structExt
Proof state before:
X : Sort u_2
I : Sort u_3
XI : I → Sort u_1
inst✝ : StructType X I XI
x x' : X
h : ∀ (i : I), structProj x i = structProj x' i
⊢ x = x'
Tactic:
rw[← structMake_structProj (I:=I) x]
Proof state after:
X : Sort u_2
I : Sort u_3
XI : I → Sort u_1
inst✝ : StructType X I XI
x x' : X
h : ∀ (i : I), structProj x i = structProj x' i
⊢ (structMake fun i => structProj x i) = x'
Theorem: SciLean.structExt
Proof state before:
X : Sort u_2
I : Sort u_3
XI : I → Sort u_1
inst✝ : StructType X I XI
x x' : X
h : ∀ (i : I), structProj x i = structProj x' i
⊢ (structMake fun i => structProj x i) = x'
Tactic:
rw[← structMake_structProj (I:=I) x']
Proof state after:
X : Sort u_2
I : Sort u_3
XI : I → Sort u_1
inst✝ : StructType X I XI
x x' : X
h : ∀ (i : I), structProj x i = structProj x' i
⊢ (structMake fun i => structProj x i) = structMake fun i => structProj x' i
Theorem: SciLean.structExt
Proof state before:
X : Sort u_2
I : Sort u_3
XI : I → Sort u_1
inst✝ : StructType X I XI
x x' : X
h : ∀ (i : I), structProj x i = structProj x' i
⊢ (structMake fun i => structProj x i) = structMake fun i => structProj x' i
Tactic:
simp[h]
Proof state after:
no goals
Theorem: SciLean.StructType.oneHot_unit
Proof state before:
X✝ : Sort ?u.24013
I : Sort ?u.24012
XI : I → Sort ?u.24011
inst✝¹ : StructType X✝ I XI
X : Type u_1
inst✝ : Zero X
x : X
⊢ oneHot () x = x
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.Measure.restrict_restrict
Proof state before:
X : Type u_1
inst✝ : MeasurableSpace X
μ : Measure X
A B : Set X
⊢ (μ.restrict A).restrict B = μ.restrict (A ∩ B)
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Measure.prod_restrict
Proof state before:
X : Type u_1
Y : Type u_2
inst✝¹ : MeasurableSpace X
inst✝ : MeasurableSpace Y
μ : Measure X
ν : Measure Y
A : Set X
B : Set Y
⊢ Measure.prod (μ.restrict A) (ν.restrict B) = (Measure.prod μ ν).restrict (A ×ˢ B)
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Measure.prod_volume
Proof state before:
X : Type u_1
Y : Type u_2
inst✝¹ : MeasureSpace X
inst✝ : MeasureSpace Y
⊢ Measure.prod volume volume = volume
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.ite_pull_measureOf
Proof state before:
X : Type u_1
inst✝¹ : MeasurableSpace X
c : Prop
inst✝ : Decidable c
μ ν : Measure X
A : Set X
⊢ ↑↑(if c then μ else ν) A = if c then ↑↑μ A else ↑↑ν A
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.ite_pull_ennreal_toReal
Proof state before:
c : Prop
inst✝ : Decidable c
x y : ENNReal
⊢ (if c then x else y).toReal = if c then x.toReal else y.toReal
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: Set.mem_fst
Proof state before:
α : Type u_1
β : Type u_2
x : α
b : β
A : Set (α × β)
⊢ (x ∈ A.fst b) = ((x, b) ∈ A)
Tactic:
rfl
Proof state after:
no goals
Theorem: Set.mem_snd
Proof state before:
α : Type u_1
β : Type u_2
a : α
y : β
A : Set (α × β)
⊢ (y ∈ A.snd a) = ((a, y) ∈ A)
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.forwardEuler.isOdeStepper
Proof 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
⊢ ∀ (t : R) (x : X), (Filter.limit (nhds 0) fun Δt' => ∂ (Δt:=Δt'), forwardEuler f t Δt x) = f t x
Tactic:
unfold forwardEuler
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
⊢ ∀ (t : R) (x : X), (Filter.limit (nhds 0) fun Δt' => ∂ (Δt:=Δt'), (x + Δt • f t x)) = f t x