internlm/Lean-Github huggingface dataset:
Theorem: SciLean.log_gaussian
Proof state before:
R : Type u_1
C : Type ?u.4719
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type ?u.4729
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiHilbert R U
μ : U
σ : R
x : U
⊢ -log (sqrt (2 * pi)) + -log σ + -‖σ⁻¹ • (x - μ)‖₂² / 2 = -‖σ⁻¹ • (x - μ)‖₂² / 2 - log σ - log (sqrt (2 * pi))
Tactic:
ring
Proof state after:
no goals
Theorem: SciLean.gaussian.arg_μx.CDifferentiableAt_rule
Proof state before:
R : Type u_1
C : Type ?u.15871
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type u_3
inst✝ : SemiHilbert R U
w : W
μ : W → U
σ : R
x : W → U
hμ : CDifferentiableAt R μ w
hx : CDifferentiableAt R x w
⊢ CDifferentiableAt R (fun w => gaussian (μ w) σ (x w)) w
Tactic:
unfold gaussian
Proof state after:
R : Type u_1
C : Type ?u.15871
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type u_3
inst✝ : SemiHilbert R U
w : W
μ : W → U
σ : R
x : W → U
hμ : CDifferentiableAt R μ w
hx : CDifferentiableAt R x w
⊢ CDifferentiableAt R
    (fun w =>
      let x' := σ⁻¹ • (x w - μ w);
      1 / (σ * Scalar.sqrt (2 * RealScalar.pi)) * Scalar.exp (-‖x'‖₂² / 2))
    w
Theorem: SciLean.gaussian.arg_μx.CDifferentiableAt_rule
Proof state before:
R : Type u_1
C : Type ?u.15871
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type u_3
inst✝ : SemiHilbert R U
w : W
μ : W → U
σ : R
x : W → U
hμ : CDifferentiableAt R μ w
hx : CDifferentiableAt R x w
⊢ CDifferentiableAt R
    (fun w =>
      let x' := σ⁻¹ • (x w - μ w);
      1 / (σ * Scalar.sqrt (2 * RealScalar.pi)) * Scalar.exp (-‖x'‖₂² / 2))
    w
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.gaussian.arg_μx.CDifferentiable_rule
Proof state before:
R : Type u_1
C : Type ?u.17313
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type u_3
inst✝ : SemiHilbert R U
μ : W → U
σ : R
x : W → U
hμ : CDifferentiable R μ
hx : CDifferentiable R x
⊢ CDifferentiable R fun w => gaussian (μ w) σ (x w)
Tactic:
intro w
Proof state after:
R : Type u_1
C : Type ?u.17313
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type u_3
inst✝ : SemiHilbert R U
μ : W → U
σ : R
x : W → U
hμ : CDifferentiable R μ
hx : CDifferentiable R x
w : W
⊢ CDifferentiableAt R (fun w => gaussian (μ w) σ (x w)) w
Theorem: SciLean.gaussian.arg_μx.CDifferentiable_rule
Proof state before:
R : Type u_1
C : Type ?u.17313
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type u_3
inst✝ : SemiHilbert R U
μ : W → U
σ : R
x : W → U
hμ : CDifferentiable R μ
hx : CDifferentiable R x
w : W
⊢ CDifferentiableAt R (fun w => gaussian (μ w) σ (x w)) w
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.gaussian.arg_μx.cderiv_rule
Proof state before:
R : Type u_1
C : Type ?u.17858
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type u_3
inst✝ : SemiHilbert R U
μ : W → U
σ : R
x : W → U
hμ : CDifferentiable R μ
hx : CDifferentiable R x
⊢ (fwdDeriv R fun w => gaussian (μ w) σ (x w)) = fun w dw =>
    let μdμ := fwdDeriv R μ w dw;
    let xdx := fwdDeriv R x w dw;
    let xdx' := σ⁻¹ • (xdx - μdμ);
    let g := gaussian μdμ.1 σ xdx.1;
    (g, -⟪xdx'.1, xdx'.2⟫_R * g)
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.gaussian.arg_μσx.CDifferentiableAt_rule
Proof state before:
R : Type u_1
C : Type ?u.21628
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type u_3
inst✝ : SemiHilbert R U
w : W
μ : W → U
σ : W → R
x : W → U
hμ : CDifferentiableAt R μ w
hσ : CDifferentiableAt R σ w
hx : CDifferentiableAt R x w
hσ' : σ w ≠ 0
⊢ CDifferentiableAt R (fun w => gaussian (μ w) (σ w) (x w)) w
Tactic:
unfold gaussian
Proof state after:
R : Type u_1
C : Type ?u.21628
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type u_3
inst✝ : SemiHilbert R U
w : W
μ : W → U
σ : W → R
x : W → U
hμ : CDifferentiableAt R μ w
hσ : CDifferentiableAt R σ w
hx : CDifferentiableAt R x w
hσ' : σ w ≠ 0
⊢ CDifferentiableAt R
    (fun w =>
      let x' := (σ w)⁻¹ • (x w - μ w);
      1 / (σ w * Scalar.sqrt (2 * RealScalar.pi)) * Scalar.exp (-‖x'‖₂² / 2))
    w
Theorem: SciLean.gaussian.arg_μσx.CDifferentiableAt_rule
Proof state before:
R : Type u_1
C : Type ?u.21628
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type u_3
inst✝ : SemiHilbert R U
w : W
μ : W → U
σ : W → R
x : W → U
hμ : CDifferentiableAt R μ w
hσ : CDifferentiableAt R σ w
hx : CDifferentiableAt R x w
hσ' : σ w ≠ 0
⊢ CDifferentiableAt R
    (fun w =>
      let x' := (σ w)⁻¹ • (x w - μ w);
      1 / (σ w * Scalar.sqrt (2 * RealScalar.pi)) * Scalar.exp (-‖x'‖₂² / 2))
    w
Tactic:
fun_prop (disch:=first | assumption | sorry_proof)
Proof state after:
no goals
Theorem: SciLean.gaussian.arg_μσx.CDifferentiableAt_rule
Proof state before:
case funProp.discharger
R : Type u_1
C : Type ?u.21628
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type u_3
inst✝ : SemiHilbert R U
w : W
μ : W → U
σ : W → R
x : W → U
hμ : CDifferentiableAt R μ w
hσ : CDifferentiableAt R σ w
hx : CDifferentiableAt R x w
hσ' : σ w ≠ 0
⊢ σ w ≠ 0
Tactic:
first | assumption | sorry_proof
Proof state after:
no goals
Theorem: SciLean.gaussian.arg_μσx.CDifferentiableAt_rule
Proof state before:
case funProp.discharger
R : Type u_1
C : Type ?u.21628
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type u_3
inst✝ : SemiHilbert R U
w : W
μ : W → U
σ : W → R
x : W → U
hμ : CDifferentiableAt R μ w
hσ : CDifferentiableAt R σ w
hx : CDifferentiableAt R x w
hσ' : σ w ≠ 0
⊢ σ w ≠ 0
Tactic:
assumption
Proof state after:
no goals
Theorem: SciLean.gaussian.arg_μσx.CDifferentiableAt_rule
Proof state before:
case funProp.discharger
R : Type u_1
C : Type ?u.21628
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type u_3
inst✝ : SemiHilbert R U
w : W
μ : W → U
σ : W → R
x : W → U
hμ : CDifferentiableAt R μ w
hσ : CDifferentiableAt R σ w
hx : CDifferentiableAt R x w
hσ' : σ w ≠ 0
⊢ 2 ≠ 0
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.gaussian.arg_μσx.CDifferentiable_rule
Proof state before:
R : Type u_1
C : Type ?u.23195
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.23233
inst✝ : SemiHilbert R U
μ σ x : W → R
hμ : CDifferentiable R μ
hσ : CDifferentiable R σ
hx : CDifferentiable R x
hσ' : ∀ (w : W), σ w ≠ 0
⊢ CDifferentiable R fun w => gaussian (μ w) (σ w) (x w)
Tactic:
intro x
Proof state after:
R : Type u_1
C : Type ?u.23195
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.23233
inst✝ : SemiHilbert R U
μ σ x✝ : W → R
hμ : CDifferentiable R μ
hσ : CDifferentiable R σ
hx : CDifferentiable R x✝
hσ' : ∀ (w : W), σ w ≠ 0
x : W
⊢ CDifferentiableAt R (fun w => gaussian (μ w) (σ w) (x✝ w)) x
Theorem: SciLean.gaussian.arg_μσx.CDifferentiable_rule
Proof state before:
R : Type u_1
C : Type ?u.23195
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.23233
inst✝ : SemiHilbert R U
μ σ x✝ : W → R
hμ : CDifferentiable R μ
hσ : CDifferentiable R σ
hx : CDifferentiable R x✝
hσ' : ∀ (w : W), σ w ≠ 0
x : W
⊢ CDifferentiableAt R (fun w => gaussian (μ w) (σ w) (x✝ w)) x
Tactic:
fun_prop (disch:=aesop)
Proof state after:
no goals
Theorem: SciLean.gaussian.arg_μσx.CDifferentiable_rule
Proof state before:
case funProp.discharger
R : Type u_1
C : Type ?u.23195
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.23233
inst✝ : SemiHilbert R U
μ σ x✝ : W → R
hμ : CDifferentiable R μ
hσ : CDifferentiable R σ
hx : CDifferentiable R x✝
hσ' : ∀ (w : W), σ w ≠ 0
x : W
⊢ σ x ≠ 0
Tactic:
aesop
Proof state after:
no goals
Theorem: SciLean.TestFunctionSpace.eval_IsSmoothLinearMap
Proof state before:
X : Type u_2
R : Type u_1
inst✝¹ : RealScalar R
inst✝ : TopologicalSpace X
space : TCOr (Vec R X) (DiscreteTopology X)
x : X
⊢ IsSmoothLinearMap R fun φ => φ x
Tactic:
constructor <;> fun_prop
Proof state after:
no goals
Theorem: SciLean.TestFunctionSpace.eval_CDifferentiable_rule'
Proof state before:
X✝ : Type ?u.13303
R : Type u_1
inst✝³ : RealScalar R
inst✝² : TopologicalSpace X✝
space : TCOr (Vec R X✝) (DiscreteTopology X✝)
W : Type u_3
inst✝¹ : Vec R W
X : Type u_2
inst✝ : Vec R X
φ : W → 𝒟 X
x : W → X
hφ : CDifferentiable R φ
hx : CDifferentiable R x
⊢ CDifferentiable R fun w => (φ w) (x w)
Tactic:
intro w
Proof state after:
X✝ : Type ?u.13303
R : Type u_1
inst✝³ : RealScalar R
inst✝² : TopologicalSpace X✝
space : TCOr (Vec R X✝) (DiscreteTopology X✝)
W : Type u_3
inst✝¹ : Vec R W
X : Type u_2
inst✝ : Vec R X
φ : W → 𝒟 X
x : W → X
hφ : CDifferentiable R φ
hx : CDifferentiable R x
w : W
⊢ CDifferentiableAt R (fun w => (φ w) (x w)) w
Theorem: SciLean.TestFunctionSpace.eval_CDifferentiable_rule'
Proof state before:
X✝ : Type ?u.13303
R : Type u_1
inst✝³ : RealScalar R
inst✝² : TopologicalSpace X✝
space : TCOr (Vec R X✝) (DiscreteTopology X✝)
W : Type u_3
inst✝¹ : Vec R W
X : Type u_2
inst✝ : Vec R X
φ : W → 𝒟 X
x : W → X
hφ : CDifferentiable R φ
hx : CDifferentiable R x
w : W
⊢ CDifferentiableAt R (fun w => (φ w) (x w)) w
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.re_float
Proof state before:
a : Float
⊢ ↑(RCLike.re a) = a
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Tactic.GTrans.HAdd.hAdd.arg_a0a1.ParametricRightInverse_rule
Proof state before:
α : Type
inst✝¹ : AddCommGroup α
inst✝ : _root_.Module ℚ α
⊢ ParametricRightInverse (fun xy => xy.1 + xy.2) α fun a z => ((1 / 2) • z + a, (1 / 2) • z - a)
Tactic:
unfold ParametricRightInverse
Proof state after:
α : Type
inst✝¹ : AddCommGroup α
inst✝ : _root_.Module ℚ α
⊢ ∀ (y c : α), (fun xy => xy.1 + xy.2) ((fun a z => ((1 / 2) • z + a, (1 / 2) • z - a)) c y) = y
Theorem: SciLean.Tactic.GTrans.HAdd.hAdd.arg_a0a1.ParametricRightInverse_rule
Proof state before:
α : Type
inst✝¹ : AddCommGroup α
inst✝ : _root_.Module ℚ α
⊢ ∀ (y c : α), (fun xy => xy.1 + xy.2) ((fun a z => ((1 / 2) • z + a, (1 / 2) • z - a)) c y) = y
Tactic:
intros
Proof state after:
α : Type
inst✝¹ : AddCommGroup α
inst✝ : _root_.Module ℚ α
y✝ c✝ : α
⊢ (fun xy => xy.1 + xy.2) ((fun a z => ((1 / 2) • z + a, (1 / 2) • z - a)) c✝ y✝) = y✝
Theorem: SciLean.Tactic.GTrans.HAdd.hAdd.arg_a0a1.ParametricRightInverse_rule
Proof state before:
α : Type
inst✝¹ : AddCommGroup α
inst✝ : _root_.Module ℚ α
y✝ c✝ : α
⊢ (fun xy => xy.1 + xy.2) ((fun a z => ((1 / 2) • z + a, (1 / 2) • z - a)) c✝ y✝) = y✝
Tactic:
simp
Proof state after:
α : Type
inst✝¹ : AddCommGroup α
inst✝ : _root_.Module ℚ α
y✝ c✝ : α
⊢ 2⁻¹ • y✝ + 2⁻¹ • y✝ = y✝
Theorem: SciLean.Tactic.GTrans.HAdd.hAdd.arg_a0a1.ParametricRightInverse_rule
Proof state before:
α : Type
inst✝¹ : AddCommGroup α
inst✝ : _root_.Module ℚ α
y✝ c✝ : α
⊢ 2⁻¹ • y✝ + 2⁻¹ • y✝ = y✝
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.odeSolve.arg_ft₀tx₀.fwdDeriv_rule
Proof state before:
R✝ : Type ?u.6372
inst✝⁶ : RCLike R✝
X✝ : Type ?u.6378
inst✝⁵ : Vec R✝ X✝
R : Type u_1
inst✝⁴ : RCLike R
W : Type u_3
inst✝³ : Vec R W
X : Type u_2
inst✝² : Vec R X
Y : Type ?u.6424
inst✝¹ : Vec R Y
Z : Type ?u.6436
inst✝ : Vec R Z
f : W → R → X → X
t₀ t : W → R
x₀ : W → X
hf :
  CDifferentiable R fun x =>
    match x with
    | (w, t, x) => f w t x
ht₀ : CDifferentiable R t₀
ht : CDifferentiable R t
hx : CDifferentiable R x₀
⊢ ∂> w, odeSolve (f w) (t₀ w) (t w) (x₀ w) = fun w dw =>
    let t₀dt₀ := ∂> t₀ w dw;
    let tdt := ∂> t₀ w dw;
    let x₀dx₀ := ∂> x₀ w dw;
    let Tf := ∂> wkx, f wkx.1 wkx.2.1 wkx.2.2;
    let F := fun t xdx =>
      let x := xdx.1;
      let dx := xdx.2;
      Tf (w, t, x) (dw, t₀dt₀.2, dx);
    let xdx := odeSolve F t₀dt₀.1 tdt.1 x₀dx₀;
    (xdx.1, xdx.2 + tdt.2 • f w tdt.1 xdx.1)
Tactic:
(conv => lhs; unfold fwdDeriv)
Proof state after:
R✝ : Type ?u.6372
inst✝⁶ : RCLike R✝
X✝ : Type ?u.6378
inst✝⁵ : Vec R✝ X✝
R : Type u_1
inst✝⁴ : RCLike R
W : Type u_3
inst✝³ : Vec R W
X : Type u_2
inst✝² : Vec R X
Y : Type ?u.6424
inst✝¹ : Vec R Y
Z : Type ?u.6436
inst✝ : Vec R Z
f : W → R → X → X
t₀ t : W → R
x₀ : W → X
hf :
  CDifferentiable R fun x =>
    match x with
    | (w, t, x) => f w t x
ht₀ : CDifferentiable R t₀
ht : CDifferentiable R t
hx : CDifferentiable R x₀
⊢ (fun x dx => ((fun w => odeSolve (f w) (t₀ w) (t w) (x₀ w)) x, ∂ (w:=x;dx), odeSolve (f w) (t₀ w) (t w) (x₀ w))) =
    fun w dw =>
    let t₀dt₀ := ∂> t₀ w dw;
    let tdt := ∂> t₀ w dw;
    let x₀dx₀ := ∂> x₀ w dw;
    let Tf := ∂> wkx, f wkx.1 wkx.2.1 wkx.2.2;
    let F := fun t xdx =>
      let x := xdx.1;
      let dx := xdx.2;
      Tf (w, t, x) (dw, t₀dt₀.2, dx);
    let xdx := odeSolve F t₀dt₀.1 tdt.1 x₀dx₀;
    (xdx.1, xdx.2 + tdt.2 • f w tdt.1 xdx.1)
Theorem: SciLean.odeSolve.arg_ft₀tx₀.fwdDeriv_rule
Proof state before:
R✝ : Type ?u.6372
inst✝⁶ : RCLike R✝
X✝ : Type ?u.6378
inst✝⁵ : Vec R✝ X✝
R : Type u_1
inst✝⁴ : RCLike R
W : Type u_3
inst✝³ : Vec R W
X : Type u_2
inst✝² : Vec R X
Y : Type ?u.6424
inst✝¹ : Vec R Y
Z : Type ?u.6436
inst✝ : Vec R Z
f : W → R → X → X
t₀ t : W → R
x₀ : W → X
hf :
  CDifferentiable R fun x =>
    match x with
    | (w, t, x) => f w t x
ht₀ : CDifferentiable R t₀
ht : CDifferentiable R t
hx : CDifferentiable R x₀
⊢ (fun x dx => ((fun w => odeSolve (f w) (t₀ w) (t w) (x₀ w)) x, ∂ (w:=x;dx), odeSolve (f w) (t₀ w) (t w) (x₀ w))) =
    fun w dw =>
    let t₀dt₀ := ∂> t₀ w dw;
    let tdt := ∂> t₀ w dw;
    let x₀dx₀ := ∂> x₀ w dw;
    let Tf := ∂> wkx, f wkx.1 wkx.2.1 wkx.2.2;
    let F := fun t xdx =>
      let x := xdx.1;
      let dx := xdx.2;
      Tf (w, t, x) (dw, t₀dt₀.2, dx);
    let xdx := odeSolve F t₀dt₀.1 tdt.1 x₀dx₀;
    (xdx.1, xdx.2 + tdt.2 • f w tdt.1 xdx.1)
Tactic:
fun_trans
Proof state after:
R✝ : Type ?u.6372
inst✝⁶ : RCLike R✝
X✝ : Type ?u.6378
inst✝⁵ : Vec R✝ X✝
R : Type u_1
inst✝⁴ : RCLike R
W : Type u_3
inst✝³ : Vec R W
X : Type u_2
inst✝² : Vec R X
Y : Type ?u.6424
inst✝¹ : Vec R Y
Z : Type ?u.6436
inst✝ : Vec R Z
f : W → R → X → X
t₀ t : W → R
x₀ : W → X
hf :
  CDifferentiable R fun x =>
    match x with
    | (w, t, x) => f w t x
ht₀ : CDifferentiable R t₀
ht : CDifferentiable R t
hx : CDifferentiable R x₀
⊢ (fun x dx =>
      (odeSolve (f x) (t₀ x) (t x) (x₀ x),
        (odeSolve (fun t xdx => ∂> (wkx:=(x, t, xdx.1);(dx, (∂> (w:=x;dx), t₀ w).2, xdx.2)), f wkx.1 wkx.2.1 wkx.2.2)
              (∂> (w:=x;dx), t₀ w).1 (∂> (w:=x;dx), t₀ w).1 (∂> (w:=x;dx), x₀ w)).2 +
          (∂> (w:=x;dx), t₀ w).2 •
            f x (∂> (w:=x;dx), t₀ w).1
              (odeSolve
                  (fun t xdx => ∂> (wkx:=(x, t, xdx.1);(dx, (∂> (w:=x;dx), t₀ w).2, xdx.2)), f wkx.1 wkx.2.1 wkx.2.2)
                  (∂> (w:=x;dx), t₀ w).1 (∂> (w:=x;dx), t₀ w).1 (∂> (w:=x;dx), x₀ w)).1)) =
    fun w dw =>
    ((odeSolve (fun t xdx => ∂> (wkx:=(w, t, xdx.1);(dw, (∂> t₀ w dw).2, xdx.2)), f wkx.1 wkx.2.1 wkx.2.2)
          (∂> t₀ w dw).1 (∂> t₀ w dw).1 (∂> x₀ w dw)).1,
      (odeSolve (fun t xdx => ∂> (wkx:=(w, t, xdx.1);(dw, (∂> t₀ w dw).2, xdx.2)), f wkx.1 wkx.2.1 wkx.2.2)
            (∂> t₀ w dw).1 (∂> t₀ w dw).1 (∂> x₀ w dw)).2 +
        (∂> t₀ w dw).2 •
          f w (∂> t₀ w dw).1
            (odeSolve (fun t xdx => ∂> (wkx:=(w, t, xdx.1);(dw, (∂> t₀ w dw).2, xdx.2)), f wkx.1 wkx.2.1 wkx.2.2)
                (∂> t₀ w dw).1 (∂> t₀ w dw).1 (∂> x₀ w dw)).1)
Theorem: SciLean.odeSolve.arg_ft₀tx₀.fwdDeriv_rule
Proof state before:
case h.h
R✝ : Type ?u.6372
inst✝⁶ : RCLike R✝
X✝ : Type ?u.6378
inst✝⁵ : Vec R✝ X✝
R : Type u_1
inst✝⁴ : RCLike R
W : Type u_3
inst✝³ : Vec R W
X : Type u_2
inst✝² : Vec R X
Y : Type ?u.6424
inst✝¹ : Vec R Y
Z : Type ?u.6436
inst✝ : Vec R Z
f : W → R → X → X
t₀ t : W → R
x₀ : W → X
hf :
  CDifferentiable R fun x =>
    match x with
    | (w, t, x) => f w t x
ht₀ : CDifferentiable R t₀
ht : CDifferentiable R t
hx : CDifferentiable R x₀
w dw : W
⊢ (odeSolve (f w) (t₀ w) (t w) (x₀ w),
      (odeSolve (fun t xdx => ∂> (wkx:=(w, t, xdx.1);(dw, (∂> (w:=w;dw), t₀ w).2, xdx.2)), f wkx.1 wkx.2.1 wkx.2.2)
            (∂> (w:=w;dw), t₀ w).1 (∂> (w:=w;dw), t₀ w).1 (∂> (w:=w;dw), x₀ w)).2 +
        (∂> (w:=w;dw), t₀ w).2 •
          f w (∂> (w:=w;dw), t₀ w).1
            (odeSolve
                (fun t xdx => ∂> (wkx:=(w, t, xdx.1);(dw, (∂> (w:=w;dw), t₀ w).2, xdx.2)), f wkx.1 wkx.2.1 wkx.2.2)
                (∂> (w:=w;dw), t₀ w).1 (∂> (w:=w;dw), t₀ w).1 (∂> (w:=w;dw), x₀ w)).1) =
    ((odeSolve (fun t xdx => ∂> (wkx:=(w, t, xdx.1);(dw, (∂> t₀ w dw).2, xdx.2)), f wkx.1 wkx.2.1 wkx.2.2)
          (∂> t₀ w dw).1 (∂> t₀ w dw).1 (∂> x₀ w dw)).1,
      (odeSolve (fun t xdx => ∂> (wkx:=(w, t, xdx.1);(dw, (∂> t₀ w dw).2, xdx.2)), f wkx.1 wkx.2.1 wkx.2.2)
            (∂> t₀ w dw).1 (∂> t₀ w dw).1 (∂> x₀ w dw)).2 +
        (∂> t₀ w dw).2 •
          f w (∂> t₀ w dw).1
            (odeSolve (fun t xdx => ∂> (wkx:=(w, t, xdx.1);(dw, (∂> t₀ w dw).2, xdx.2)), f wkx.1 wkx.2.1 wkx.2.2)
                (∂> t₀ w dw).1 (∂> t₀ w dw).1 (∂> x₀ w dw)).1)
Tactic:
simp[fwdDeriv]
Proof state after:
case h.h
R✝ : Type ?u.6372
inst✝⁶ : RCLike R✝
X✝ : Type ?u.6378
inst✝⁵ : Vec R✝ X✝
R : Type u_1
inst✝⁴ : RCLike R
W : Type u_3
inst✝³ : Vec R W
X : Type u_2
inst✝² : Vec R X
Y : Type ?u.6424
inst✝¹ : Vec R Y
Z : Type ?u.6436
inst✝ : Vec R Z
f : W → R → X → X
t₀ t : W → R
x₀ : W → X
hf :
  CDifferentiable R fun x =>
    match x with
    | (w, t, x) => f w t x
ht₀ : CDifferentiable R t₀
ht : CDifferentiable R t
hx : CDifferentiable R x₀
w dw : W
⊢ odeSolve (f w) (t₀ w) (t w) (x₀ w) =
    (odeSolve (fun t xdx => (f w t xdx.1, ∂ (wkx:=(w, t, xdx.1);(dw, ∂ t₀ w dw, xdx.2)), f wkx.1 wkx.2.1 wkx.2.2))
        (t₀ w) (t₀ w) (x₀ w, ∂ x₀ w dw)).1
Theorem: SciLean.odeSolve.arg_ft₀tx₀.fwdDeriv_rule
Proof state before:
case h.h
R✝ : Type ?u.6372
inst✝⁶ : RCLike R✝
X✝ : Type ?u.6378
inst✝⁵ : Vec R✝ X✝
R : Type u_1
inst✝⁴ : RCLike R
W : Type u_3
inst✝³ : Vec R W
X : Type u_2
inst✝² : Vec R X
Y : Type ?u.6424
inst✝¹ : Vec R Y
Z : Type ?u.6436
inst✝ : Vec R Z
f : W → R → X → X
t₀ t : W → R
x₀ : W → X
hf :
  CDifferentiable R fun x =>
    match x with
    | (w, t, x) => f w t x
ht₀ : CDifferentiable R t₀
ht : CDifferentiable R t
hx : CDifferentiable R x₀
w dw : W
⊢ odeSolve (f w) (t₀ w) (t w) (x₀ w) =
    (odeSolve (fun t xdx => (f w t xdx.1, ∂ (wkx:=(w, t, xdx.1);(dw, ∂ t₀ w dw, xdx.2)), f wkx.1 wkx.2.1 wkx.2.2))
        (t₀ w) (t₀ w) (x₀ w, ∂ x₀ w dw)).1
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.odeSolve.arg_ft₀tx₀.fwdDeriv_rule
Proof state before:
R✝ : Type ?u.6372
inst✝⁶ : RCLike R✝
X✝ : Type ?u.6378
inst✝⁵ : Vec R✝ X✝
R : Type u_1
inst✝⁴ : RCLike R
W : Type u_3
inst✝³ : Vec R W
X : Type u_2
inst✝² : Vec R X
Y : Type ?u.6424
inst✝¹ : Vec R Y
Z : Type ?u.6436
inst✝ : Vec R Z
f : W → R → X → X
t₀ t : W → R
x₀ : W → X
hf :
  CDifferentiable R fun x =>
    match x with
    | (w, t, x) => f w t x
ht₀ : CDifferentiable R t₀
ht : CDifferentiable R t
hx : CDifferentiable R x₀
⊢ ∂> w, odeSolve (f w) (t₀ w) (t w) (x₀ w) = fun w dw =>
    let t₀dt₀ := ∂> t₀ w dw;
    let tdt := ∂> t₀ w dw;
    let x₀dx₀ := ∂> x₀ w dw;
    let Tf := ∂> wkx, f wkx.1 wkx.2.1 wkx.2.2;
    let F := fun t xdx =>
      let x := xdx.1;
      let dx := xdx.2;
      Tf (w, t, x) (dw, t₀dt₀.2, dx);
    let xdx := odeSolve F t₀dt₀.1 tdt.1 x₀dx₀;
    (xdx.1, xdx.2 + tdt.2 • f w tdt.1 xdx.1)
Tactic:
conv => lhs; unfold fwdDeriv
Proof state after:
R✝ : Type ?u.6372
inst✝⁶ : RCLike R✝
X✝ : Type ?u.6378
inst✝⁵ : Vec R✝ X✝
R : Type u_1
inst✝⁴ : RCLike R
W : Type u_3
inst✝³ : Vec R W
X : Type u_2
inst✝² : Vec R X
Y : Type ?u.6424
inst✝¹ : Vec R Y
Z : Type ?u.6436
inst✝ : Vec R Z
f : W → R → X → X
t₀ t : W → R
x₀ : W → X
hf :
  CDifferentiable R fun x =>
    match x with
    | (w, t, x) => f w t x
ht₀ : CDifferentiable R t₀
ht : CDifferentiable R t
hx : CDifferentiable R x₀
⊢ (fun x dx => ((fun w => odeSolve (f w) (t₀ w) (t w) (x₀ w)) x, ∂ (w:=x;dx), odeSolve (f w) (t₀ w) (t w) (x₀ w))) =
    fun w dw =>
    let t₀dt₀ := ∂> t₀ w dw;
    let tdt := ∂> t₀ w dw;
    let x₀dx₀ := ∂> x₀ w dw;
    let Tf := ∂> wkx, f wkx.1 wkx.2.1 wkx.2.2;
    let F := fun t xdx =>
      let x := xdx.1;
      let dx := xdx.2;
      Tf (w, t, x) (dw, t₀dt₀.2, dx);
    let xdx := odeSolve F t₀dt₀.1 tdt.1 x₀dx₀;
    (xdx.1, xdx.2 + tdt.2 • f w tdt.1 xdx.1)
Theorem: SciLean.odeSolve.arg_x₀.semiAdjoint_rule
Proof state before:
R✝ : Type ?u.20793
inst✝⁶ : RCLike R✝
X✝ : Type ?u.20799
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.20845
inst✝¹ : SemiInnerProductSpace R Y
Z : Type ?u.20857
inst✝ : SemiInnerProductSpace R Z
f : R → X → X
t₀ t : R
x₀ : W → X
hf : ∀ (t : R), HasSemiAdjoint R (f t)
hx₀ : HasSemiAdjoint R x₀
⊢ (semiAdjoint R fun w => odeSolve f t₀ t (x₀ w)) = fun x₀' =>
    let f' := fun s y => -semiAdjoint R (f s) y;
    let y := odeSolve f' t t₀ x₀';
    semiAdjoint R x₀ y
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.odeSolve.arg_x₀.revCDeriv_rule
Proof 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
Proof 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)
Theorem: SciLean.odeSolve.arg_x₀.revCDeriv_rule
Proof 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
Proof 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))