internlm/Lean-Github huggingface dataset:
Theorem: SciLean.Scalar.log.arg_x.revDeriv_rule
Proof state before:
R✝ : Type ?u.29295
C : Type ?u.29294
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.29304
inst✝⁴ : Vec C W✝
U✝ : Type ?u.29327
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.29349
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
x : U → R
hx : HasAdjDiff R x
hu : ∀ (u : U), x u ≠ 0
⊢ (fun x_1 => ((fun u => log (x u)) x_1, semiAdjoint R (cderiv R (fun u => log (x u)) x_1))) = fun u =>
    let xdx := (x u, semiAdjoint R (cderiv R x u));
    (log xdx.1, fun dy => xdx.2 ((abs (x u))⁻¹ * dy))
Tactic:
fun_trans (disch:=aesop) only [fwdDeriv, smul_push, ftrans_simp]
Proof state after:
no goals
Theorem: SciLean.Scalar.log.arg_x.revDeriv_rule
Proof state before:
case funProp.discharger
R✝ : Type ?u.29295
C : Type ?u.29294
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.29304
inst✝⁴ : Vec C W✝
U✝ : Type ?u.29327
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.29349
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
x✝ : U → R
hx : HasAdjDiff R x✝
hu : ∀ (u : U), x✝ u ≠ 0
x : U
⊢ x✝ x ≠ 0
Tactic:
aesop
Proof state after:
no goals
Theorem: SciLean.foo1_spec
Proof state before:
R : Type
inst✝⁵ : RealScalar R
W : Type ?u.13209
inst✝⁴ : SemiHilbert R W
X : Type ?u.13239
inst✝³ : SemiHilbert R X
Y : Type ?u.13263
inst✝² : SemiHilbert R Y
Z : Type ?u.13287
inst✝¹ : SemiHilbert R Z
inst✝ : MeasureSpace R
t : R
⊢ foo1 t = if 0 < t ∧ t < 1 then 1 else 0
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.foo2_spec
Proof state before:
R : Type
inst✝⁵ : RealScalar R
W : Type ?u.33122
inst✝⁴ : SemiHilbert R W
X : Type ?u.33152
inst✝³ : SemiHilbert R X
Y : Type ?u.33176
inst✝² : SemiHilbert R Y
Z : Type ?u.33200
inst✝¹ : SemiHilbert R Z
inst✝ : MeasureSpace R
t : R
⊢ foo2 t = if 0 < t ∧ t < 1 then 1 else 0
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.ContCDiffMapFD_eta
Proof state before:
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_3
inst✝⁶ : Vec K Y
Z : Type ?u.13631
inst✝⁵ : Vec K Z
W : Type ?u.13642
inst✝⁴ : Vec K W
ι : Type ?u.13653
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.13680
inst✝ : (i : ι) → Vec K (E i)
n : ℕ∞
f : X ⟿FD[K,n] Y
⊢ (fun x ⟿FD[K,n] f x) = f
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.ContCDiffMapFD_eval_fwdDeriv
Proof state before:
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_3
inst✝⁶ : Vec K Y
Z : Type ?u.14527
inst✝⁵ : Vec K Z
W : Type ?u.14538
inst✝⁴ : Vec K W
ι : Type ?u.14549
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.14576
inst✝ : (i : ι) → Vec K (E i)
n : ℕ∞
f : X ⟿FD[K,n] Y
⊢ (fwdDeriv K fun x => f x) = f.FD
Tactic:
unfold ContCDiffMapFD.FD fwdDeriv
Proof state after:
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_3
inst✝⁶ : Vec K Y
Z : Type ?u.14527
inst✝⁵ : Vec K Z
W : Type ?u.14538
inst✝⁴ : Vec K W
ι : Type ?u.14549
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.14576
inst✝ : (i : ι) → Vec K (E i)
n : ℕ∞
f : X ⟿FD[K,n] Y
⊢ (fun x dx => ((fun x => f x) x, ∂ (x:=x;dx), f x)) = fun x dx => f.toFun x dx
Theorem: SciLean.ContCDiffMapFD_eval_fwdDeriv
Proof state before:
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_3
inst✝⁶ : Vec K Y
Z : Type ?u.14527
inst✝⁵ : Vec K Z
W : Type ?u.14538
inst✝⁴ : Vec K W
ι : Type ?u.14549
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.14576
inst✝ : (i : ι) → Vec K (E i)
n : ℕ∞
f : X ⟿FD[K,n] Y
⊢ (fun x dx => ((fun x => f x) x, ∂ (x:=x;dx), f x)) = fun x dx => f.toFun x dx
Tactic:
simp[DFunLike.coe]
Proof state after:
no goals
Theorem: SciLean.ContCDiffMapFD_eval_cdifferentiable
Proof state before:
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_3
inst✝⁶ : Vec K Y
Z : Type ?u.17138
inst✝⁵ : Vec K Z
W : Type ?u.17149
inst✝⁴ : Vec K W
ι : Type ?u.17160
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.17187
inst✝ : (i : ι) → Vec K (E i)
n : ℕ∞
f : X ⟿FD[K,n] Y
h : 0 < n
⊢ CDifferentiable K fun x => f x
Tactic:
simp[DFunLike.coe]
Proof state after:
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_3
inst✝⁶ : Vec K Y
Z : Type ?u.17138
inst✝⁵ : Vec K Z
W : Type ?u.17149
inst✝⁴ : Vec K W
ι : Type ?u.17160
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.17187
inst✝ : (i : ι) → Vec K (E i)
n : ℕ∞
f : X ⟿FD[K,n] Y
h : 0 < n
⊢ CDifferentiable K fun x => (f.toFun x 0).1
Theorem: SciLean.ContCDiffMapFD_eval_cdifferentiable
Proof state before:
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_3
inst✝⁶ : Vec K Y
Z : Type ?u.17138
inst✝⁵ : Vec K Z
W : Type ?u.17149
inst✝⁴ : Vec K W
ι : Type ?u.17160
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.17187
inst✝ : (i : ι) → Vec K (E i)
n : ℕ∞
f : X ⟿FD[K,n] Y
h : 0 < n
⊢ CDifferentiable K fun x => (f.toFun x 0).1
Tactic:
apply CDifferentaible.ContCDiff_rule
Proof state after:
case hf
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_3
inst✝⁶ : Vec K Y
Z : Type ?u.17138
inst✝⁵ : Vec K Z
W : Type ?u.17149
inst✝⁴ : Vec K W
ι : Type ?u.17160
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.17187
inst✝ : (i : ι) → Vec K (E i)
n : ℕ∞
f : X ⟿FD[K,n] Y
h : 0 < n
⊢ ContCDiff K ?n fun x => (f.toFun x 0).1

case h
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_3
inst✝⁶ : Vec K Y
Z : Type ?u.17138
inst✝⁵ : Vec K Z
W : Type ?u.17149
inst✝⁴ : Vec K W
ι : Type ?u.17160
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.17187
inst✝ : (i : ι) → Vec K (E i)
n : ℕ∞
f : X ⟿FD[K,n] Y
h : 0 < n
⊢ 0 < ?n

case n
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_3
inst✝⁶ : Vec K Y
Z : Type ?u.17138
inst✝⁵ : Vec K Z
W : Type ?u.17149
inst✝⁴ : Vec K W
ι : Type ?u.17160
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.17187
inst✝ : (i : ι) → Vec K (E i)
n : ℕ∞
f : X ⟿FD[K,n] Y
h : 0 < n
⊢ ℕ∞
Theorem: SciLean.ContCDiffMapFD_eval_cdifferentiable
Proof state before:
case hf
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_3
inst✝⁶ : Vec K Y
Z : Type ?u.17138
inst✝⁵ : Vec K Z
W : Type ?u.17149
inst✝⁴ : Vec K W
ι : Type ?u.17160
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.17187
inst✝ : (i : ι) → Vec K (E i)
n : ℕ∞
f : X ⟿FD[K,n] Y
h : 0 < n
⊢ ContCDiff K ?n fun x => (f.toFun x 0).1

case h
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_3
inst✝⁶ : Vec K Y
Z : Type ?u.17138
inst✝⁵ : Vec K Z
W : Type ?u.17149
inst✝⁴ : Vec K W
ι : Type ?u.17160
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.17187
inst✝ : (i : ι) → Vec K (E i)
n : ℕ∞
f : X ⟿FD[K,n] Y
h : 0 < n
⊢ 0 < ?n

case n
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_3
inst✝⁶ : Vec K Y
Z : Type ?u.17138
inst✝⁵ : Vec K Z
W : Type ?u.17149
inst✝⁴ : Vec K W
ι : Type ?u.17160
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.17187
inst✝ : (i : ι) → Vec K (E i)
n : ℕ∞
f : X ⟿FD[K,n] Y
h : 0 < n
⊢ ℕ∞
Tactic:
apply ContCDiffMapFD.is_cont_cdiff_map
Proof state after:
case h
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_3
inst✝⁶ : Vec K Y
Z : Type ?u.17138
inst✝⁵ : Vec K Z
W : Type ?u.17149
inst✝⁴ : Vec K W
ι : Type ?u.17160
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.17187
inst✝ : (i : ι) → Vec K (E i)
n : ℕ∞
f : X ⟿FD[K,n] Y
h : 0 < n
⊢ 0 < n
Theorem: SciLean.ContCDiffMapFD_eval_cdifferentiable
Proof state before:
case h
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_3
inst✝⁶ : Vec K Y
Z : Type ?u.17138
inst✝⁵ : Vec K Z
W : Type ?u.17149
inst✝⁴ : Vec K W
ι : Type ?u.17160
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.17187
inst✝ : (i : ι) → Vec K (E i)
n : ℕ∞
f : X ⟿FD[K,n] Y
h : 0 < n
⊢ 0 < n
Tactic:
assumption
Proof state after:
no goals
Theorem: SciLean.ContCDiffMapFD_eval_cdifferentiable'
Proof state before:
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_3
inst✝⁶ : Vec K Y
Z : Type ?u.18366
inst✝⁵ : Vec K Z
W : Type ?u.18377
inst✝⁴ : Vec K W
ι : Type ?u.18388
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.18415
inst✝ : (i : ι) → Vec K (E i)
n : ℕ∞
f : X ⟿FD[K,⊤] Y
⊢ CDifferentiable K fun x => f x
Tactic:
fun_prop (disch:=apply ENat.zero_lt_top)
Proof state after:
no goals
Theorem: SciLean.ContCDiffMapFD_eval_cdifferentiable'
Proof state before:
case funProp.discharger
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_3
inst✝⁶ : Vec K Y
Z : Type ?u.18366
inst✝⁵ : Vec K Z
W : Type ?u.18377
inst✝⁴ : Vec K W
ι : Type ?u.18388
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.18415
inst✝ : (i : ι) → Vec K (E i)
n : ℕ∞
f : X ⟿FD[K,⊤] Y
⊢ 0 < ⊤
Tactic:
apply ENat.zero_lt_top
Proof state after:
no goals
Theorem: SciLean.ContCDiffMapFD.FD_fst
Proof state before:
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_3
inst✝⁶ : Vec K Y
Z : Type ?u.18778
inst✝⁵ : Vec K Z
W : Type ?u.18789
inst✝⁴ : Vec K W
ι : Type ?u.18800
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.18827
inst✝ : (i : ι) → Vec K (E i)
n : ℕ∞
f : X ⟿FD[K,n] Y
x dx : X
⊢ (f.FD x dx).1 = f x
Tactic:
rw[← ContCDiffMapFD_eval_fwdDeriv]
Proof state after:
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_3
inst✝⁶ : Vec K Y
Z : Type ?u.18778
inst✝⁵ : Vec K Z
W : Type ?u.18789
inst✝⁴ : Vec K W
ι : Type ?u.18800
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.18827
inst✝ : (i : ι) → Vec K (E i)
n : ℕ∞
f : X ⟿FD[K,n] Y
x dx : X
⊢ (fwdDeriv K (fun x => f x) x dx).1 = f x
Theorem: SciLean.ContCDiffMapFD.FD_fst
Proof state before:
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_3
inst✝⁶ : Vec K Y
Z : Type ?u.18778
inst✝⁵ : Vec K Z
W : Type ?u.18789
inst✝⁴ : Vec K W
ι : Type ?u.18800
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.18827
inst✝ : (i : ι) → Vec K (E i)
n : ℕ∞
f : X ⟿FD[K,n] Y
x dx : X
⊢ (fwdDeriv K (fun x => f x) x dx).1 = f x
Tactic:
unfold fwdDeriv
Proof state after:
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_3
inst✝⁶ : Vec K Y
Z : Type ?u.18778
inst✝⁵ : Vec K Z
W : Type ?u.18789
inst✝⁴ : Vec K W
ι : Type ?u.18800
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.18827
inst✝ : (i : ι) → Vec K (E i)
n : ℕ∞
f : X ⟿FD[K,n] Y
x dx : X
⊢ ((fun x => f x) x, ∂ (x:=x;dx), f x).1 = f x
Theorem: SciLean.ContCDiffMapFD.FD_fst
Proof state before:
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_3
inst✝⁶ : Vec K Y
Z : Type ?u.18778
inst✝⁵ : Vec K Z
W : Type ?u.18789
inst✝⁴ : Vec K W
ι : Type ?u.18800
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.18827
inst✝ : (i : ι) → Vec K (E i)
n : ℕ∞
f : X ⟿FD[K,n] Y
x dx : X
⊢ ((fun x => f x) x, ∂ (x:=x;dx), f x).1 = f x
Tactic:
simp
Proof state after:
no goals
Theorem: SciLean.ContCDiffMapFD.add_apply
Proof state before:
K : Type u_3
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_1
inst✝⁶ : Vec K Y
Z : Type ?u.33045
inst✝⁵ : Vec K Z
W : Type ?u.33056
inst✝⁴ : Vec K W
ι : Type ?u.33067
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.33094
inst✝ : (i : ι) → Vec K (E i)
n : ℕ∞
f g : X ⟿FD[K,n] Y
x : X
r : K
⊢ (f + g) x = f x + g x
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.ContCDiffMapFD.sub_apply
Proof state before:
K : Type u_3
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_1
inst✝⁶ : Vec K Y
Z : Type ?u.34681
inst✝⁵ : Vec K Z
W : Type ?u.34692
inst✝⁴ : Vec K W
ι : Type ?u.34703
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.34730
inst✝ : (i : ι) → Vec K (E i)
n : ℕ∞
f g : X ⟿FD[K,n] Y
x : X
r : K
⊢ (f - g) x = f x - g x
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.ContCDiffMapFD.neg_apply
Proof state before:
K : Type u_3
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_1
inst✝⁶ : Vec K Y
Z : Type ?u.35781
inst✝⁵ : Vec K Z
W : Type ?u.35792
inst✝⁴ : Vec K W
ι : Type ?u.35803
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.35830
inst✝ : (i : ι) → Vec K (E i)
n : ℕ∞
f g : X ⟿FD[K,n] Y
x : X
r : K
⊢ (-f) x = -f x
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.ContCDiffMapFD.smul_apply
Proof state before:
K : Type u_3
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_1
inst✝⁶ : Vec K Y
Z : Type ?u.36439
inst✝⁵ : Vec K Z
W : Type ?u.36450
inst✝⁴ : Vec K W
ι : Type ?u.36461
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.36488
inst✝ : (i : ι) → Vec K (E i)
n : ℕ∞
f g : X ⟿FD[K,n] Y
x : X
r : K
⊢ (r • f) x = r • f x
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.ContCDiffMapFD.zero_apply
Proof state before:
K : Type u_3
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_1
inst✝⁶ : Vec K Y
Z : Type ?u.38378
inst✝⁵ : Vec K Z
W : Type ?u.38389
inst✝⁴ : Vec K W
ι : Type ?u.38400
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.38427
inst✝ : (i : ι) → Vec K (E i)
n : ℕ∞
f g : X ⟿FD[K,n] Y
x : X
r : K
⊢ 0 x = 0
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.ContCDiffMapFD_eval_CDifferentiable
Proof state before:
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_3
inst✝⁶ : Vec K Y
Z : Type ?u.59271
inst✝⁵ : Vec K Z
W : Type ?u.59282
inst✝⁴ : Vec K W
ι : Type ?u.59293
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.59320
inst✝ : (i : ι) → Vec K (E i)
n : ℕ∞
h : 0 < n
⊢ CDifferentiable K fun fx => fx.1 fx.2
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.ContCDiffMapFD_eval_CDifferentiable'
Proof state before:
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_3
inst✝⁶ : Vec K Y
Z : Type ?u.59717
inst✝⁵ : Vec K Z
W : Type ?u.59728
inst✝⁴ : Vec K W
ι : Type ?u.59739
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.59766
inst✝ : (i : ι) → Vec K (E i)
n : ℕ∞
⊢ CDifferentiable K fun fx => fx.1 fx.2
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.ContCDiffMapFD_apply_CDifferentiable
Proof state before:
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_3
inst✝⁶ : Vec K Y
Z : Type ?u.60106
inst✝⁵ : Vec K Z
W : Type u_4
inst✝⁴ : Vec K W
ι : Type ?u.60128
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.60155
inst✝ : (i : ι) → Vec K (E i)
n : ℕ∞
f : W → X ⟿FD[K,⊤] Y
g : W → X
hf : CDifferentiable K f
hg : CDifferentiable K g
⊢ CDifferentiable K fun w => (f w) (g w)
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.ContCDiffMapFD_apply_CDifferentiableAt
Proof state before:
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_3
inst✝⁶ : Vec K Y
Z : Type ?u.60517
inst✝⁵ : Vec K Z
W : Type u_4
inst✝⁴ : Vec K W
ι : Type ?u.60539
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.60566
inst✝ : (i : ι) → Vec K (E i)
n : ℕ∞
f : W → X ⟿FD[K,⊤] Y
g : W → X
w : W
hf : CDifferentiableAt K f w
hg : CDifferentiableAt K g w
⊢ CDifferentiableAt K (fun w => (f w) (g w)) w
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.ContCDiffMapFD_fwdDeriv_rule
Proof state before:
K : Type u_4
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_1
inst✝⁶ : Vec K Y
Z : Type u_3
inst✝⁵ : Vec K Z
W : Type u_5
inst✝⁴ : Vec K W
ι : Type ?u.62779
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.62806
inst✝ : (i : ι) → Vec K (E i)
n : ℕ∞
f : W → (X ⟿FD[K,⊤] Y) × Z
g : W → X
⊢ (fwdDeriv K fun w => (f w).1 (g w)) = fun w dw =>
    let fdfz := fwdDeriv K f w dw;
    let xdx := fwdDeriv K g w dw;
    let fw := fdfz.1.1;
    let df := fdfz.2.1;
    let zdz := fw.FD xdx.1 xdx.2;
    (zdz.1, df xdx.1 + zdz.2)
Tactic:
unfold fwdDeriv
Proof state after:
K : Type u_4
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_1
inst✝⁶ : Vec K Y
Z : Type u_3
inst✝⁵ : Vec K Z
W : Type u_5
inst✝⁴ : Vec K W
ι : Type ?u.62779
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.62806
inst✝ : (i : ι) → Vec K (E i)
n : ℕ∞
f : W → (X ⟿FD[K,⊤] Y) × Z
g : W → X
⊢ (fun x dx => ((fun w => (f w).1 (g w)) x, ∂ (w:=x;dx), (f w).1 (g w))) = fun w dw =>
    let fdfz := (f w, ∂ f w dw);
    let xdx := (g w, ∂ g w dw);
    let fw := fdfz.1.1;
    let df := fdfz.2.1;
    let zdz := fw.FD xdx.1 xdx.2;
    (zdz.1, df xdx.1 + zdz.2)
Theorem: SciLean.ContCDiffMapFD_fwdDeriv_rule
Proof state before:
K : Type u_4
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_1
inst✝⁶ : Vec K Y
Z : Type u_3
inst✝⁵ : Vec K Z
W : Type u_5
inst✝⁴ : Vec K W
ι : Type ?u.62779
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.62806
inst✝ : (i : ι) → Vec K (E i)
n : ℕ∞
f : W → (X ⟿FD[K,⊤] Y) × Z
g : W → X
⊢ (fun x dx => ((fun w => (f w).1 (g w)) x, ∂ (w:=x;dx), (f w).1 (g w))) = fun w dw =>
    let fdfz := (f w, ∂ f w dw);
    let xdx := (g w, ∂ g w dw);
    let fw := fdfz.1.1;
    let df := fdfz.2.1;
    let zdz := fw.FD xdx.1 xdx.2;
    (zdz.1, df xdx.1 + zdz.2)
Tactic:
fun_trans
Proof state after:
no goals
Theorem: SciLean.CDifferentiableAt.id_rule
Proof state before:
K : Type u_1
inst✝⁵ : RCLike K
X : Type u_2
inst✝⁴ : Vec K X
Y : Type ?u.1594
inst✝³ : Vec K Y
Z : Type ?u.1605
inst✝² : Vec K Z
ι : Type ?u.1616
inst✝¹ : IndexType ι
E : ι → Type ?u.1625
inst✝ : (i : ι) → Vec K (E i)
x : X
⊢ CDifferentiableAt K (fun x => x) x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.CDifferentiable.id_rule
Proof state before:
K : Type u_1
inst✝⁵ : RCLike K
X : Type u_2
inst✝⁴ : Vec K X
Y : Type ?u.1712
inst✝³ : Vec K Y
Z : Type ?u.1723
inst✝² : Vec K Z
ι : Type ?u.1734
inst✝¹ : IndexType ι
E : ι → Type ?u.1743
inst✝ : (i : ι) → Vec K (E i)
⊢ CDifferentiable K fun x => x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.CDifferentiableAt.const_rule
Proof state before:
K : Type u_1
inst✝⁵ : RCLike K
X : Type u_2
inst✝⁴ : Vec K X
Y : Type u_3
inst✝³ : Vec K Y
Z : Type ?u.1834
inst✝² : Vec K Z
ι : Type ?u.1845
inst✝¹ : IndexType ι
E : ι → Type ?u.1854
inst✝ : (i : ι) → Vec K (E i)
y : Y
x : X
⊢ CDifferentiableAt K (fun x => y) x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.CDifferentiable.const_rule
Proof state before:
K : Type u_1
inst✝⁵ : RCLike K
X : Type u_2
inst✝⁴ : Vec K X
Y : Type u_3
inst✝³ : Vec K Y
Z : Type ?u.1974
inst✝² : Vec K Z
ι : Type ?u.1985
inst✝¹ : IndexType ι
E : ι → Type ?u.1994
inst✝ : (i : ι) → Vec K (E i)
y : Y
⊢ CDifferentiable K fun x => y
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.CDifferentiableAt.comp_rule
Proof state before:
K : Type u_1
inst✝⁵ : RCLike K
X : Type u_4
inst✝⁴ : Vec K X
Y : Type u_2
inst✝³ : Vec K Y
Z : Type u_3
inst✝² : Vec K Z
ι : Type ?u.2188
inst✝¹ : IndexType ι
E : ι → Type ?u.2197
inst✝ : (i : ι) → Vec K (E i)
f : Y → Z
g : X → Y
x : X
hf : CDifferentiableAt K f (g x)
hg : CDifferentiableAt K g x
⊢ CDifferentiableAt K (fun x => f (g x)) x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.CDifferentiable.comp_rule
Proof state before:
K : Type u_1
inst✝⁵ : RCLike K
X : Type u_4
inst✝⁴ : Vec K X
Y : Type u_2
inst✝³ : Vec K Y
Z : Type u_3
inst✝² : Vec K Z
ι : Type ?u.2389
inst✝¹ : IndexType ι
E : ι → Type ?u.2398
inst✝ : (i : ι) → Vec K (E i)
f : Y → Z
g : X → Y
hf : CDifferentiable K f
hg : CDifferentiable K g
⊢ CDifferentiable K fun x => f (g x)
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.CDifferentiableAt.apply_rule
Proof state before:
K : Type u_1
inst✝⁵ : RCLike K
X : Type ?u.2618
inst✝⁴ : Vec K X
Y : Type ?u.2631
inst✝³ : Vec K Y
Z : Type ?u.2642
inst✝² : Vec K Z
ι : Type u_2
inst✝¹ : IndexType ι
E : ι → Type u_3
inst✝ : (i : ι) → Vec K (E i)
i : ι
x : (i : ι) → E i
⊢ CDifferentiableAt K (fun x => x i) x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.CDifferentiable.apply_rule
Proof state before:
K : Type u_1
inst✝⁵ : RCLike K
X : Type ?u.3340
inst✝⁴ : Vec K X
Y : Type ?u.3353
inst✝³ : Vec K Y
Z : Type ?u.3364
inst✝² : Vec K Z
ι : Type u_2
inst✝¹ : IndexType ι
E : ι → Type u_3
inst✝ : (i : ι) → Vec K (E i)
i : ι
⊢ CDifferentiable K fun x => x i
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.CDifferentiableAt.pi_rule
Proof state before:
K : Type u_1
inst✝⁵ : RCLike K
X : Type u_2
inst✝⁴ : Vec K X
Y : Type ?u.4136
inst✝³ : Vec K Y
Z : Type ?u.4147
inst✝² : Vec K Z
ι : Type u_4
inst✝¹ : IndexType ι
E : ι → Type u_3
inst✝ : (i : ι) → Vec K (E i)
f : X → (i : ι) → E i
x : X
hf : ∀ (i : ι), CDifferentiableAt K (fun x => f x i) x
⊢ CDifferentiableAt K (fun x i => f x i) x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.CDifferentiable.pi_rule
Proof state before:
K : Type u_1
inst✝⁵ : RCLike K
X : Type u_2
inst✝⁴ : Vec K X
Y : Type ?u.4909
inst✝³ : Vec K Y
Z : Type ?u.4920
inst✝² : Vec K Z
ι : Type u_4
inst✝¹ : IndexType ι
E : ι → Type u_3
inst✝ : (i : ι) → Vec K (E i)
f : X → (i : ι) → E i
hf : ∀ (i : ι), CDifferentiable K fun x => f x i
⊢ CDifferentiable K fun x i => f x i
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Prod.mk.arg_fstsnd.CDifferentiableAt_rule
Proof state before:
K✝ : Type ?u.6292
inst✝¹¹ : RCLike K✝
X✝ : Type ?u.6298
inst✝¹⁰ : Vec K✝ X✝
Y✝ : Type ?u.6311
inst✝⁹ : Vec K✝ Y✝
Z✝ : Type ?u.6322
inst✝⁸ : Vec K✝ Z✝
ι✝ : Type ?u.6333
inst✝⁷ : IndexType ι✝
E✝ : ι✝ → Type ?u.6342
inst✝⁶ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_1
inst✝⁵ : RCLike K
X : Type u_2
inst✝⁴ : Vec K X
Y : Type u_3
inst✝³ : Vec K Y
Z : Type u_4
inst✝² : Vec K Z
ι : Type ?u.6399
inst✝¹ : IndexType ι
E : ι → Type ?u.6408
inst✝ : (i : ι) → Vec K (E i)
x : X
g : X → Y
hg : CDifferentiableAt K g x
f : X → Z
hf : CDifferentiableAt K f x
⊢ CDifferentiableAt K (fun x => (g x, f x)) x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Prod.mk.arg_fstsnd.CDifferentiable_rule
Proof state before:
K✝ : Type ?u.6642
inst✝¹¹ : RCLike K✝
X✝ : Type ?u.6648
inst✝¹⁰ : Vec K✝ X✝
Y✝ : Type ?u.6661
inst✝⁹ : Vec K✝ Y✝
Z✝ : Type ?u.6672
inst✝⁸ : Vec K✝ Z✝
ι✝ : Type ?u.6683
inst✝⁷ : IndexType ι✝
E✝ : ι✝ → Type ?u.6692
inst✝⁶ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_1
inst✝⁵ : RCLike K
X : Type u_2
inst✝⁴ : Vec K X
Y : Type u_3
inst✝³ : Vec K Y
Z : Type u_4
inst✝² : Vec K Z
ι : Type ?u.6749
inst✝¹ : IndexType ι
E : ι → Type ?u.6758
inst✝ : (i : ι) → Vec K (E i)
g : X → Y
hg : CDifferentiable K g
f : X → Z
hf : CDifferentiable K f
⊢ CDifferentiable K fun x => (g x, f x)
Tactic:
intro x
Proof state after:
K✝ : Type ?u.6642
inst✝¹¹ : RCLike K✝
X✝ : Type ?u.6648
inst✝¹⁰ : Vec K✝ X✝
Y✝ : Type ?u.6661
inst✝⁹ : Vec K✝ Y✝
Z✝ : Type ?u.6672
inst✝⁸ : Vec K✝ Z✝
ι✝ : Type ?u.6683
inst✝⁷ : IndexType ι✝
E✝ : ι✝ → Type ?u.6692
inst✝⁶ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_1
inst✝⁵ : RCLike K
X : Type u_2
inst✝⁴ : Vec K X
Y : Type u_3
inst✝³ : Vec K Y
Z : Type u_4
inst✝² : Vec K Z
ι : Type ?u.6749
inst✝¹ : IndexType ι
E : ι → Type ?u.6758
inst✝ : (i : ι) → Vec K (E i)
g : X → Y
hg : CDifferentiable K g
f : X → Z
hf : CDifferentiable K f
x : X
⊢ CDifferentiableAt K (fun x => (g x, f x)) x