internlm/Lean-Github huggingface dataset:
Theorem: SciLean.Scalar.exp.arg_x.HasAdjDiff_rule
Proof state before:
case left
R : Type u_3
C : Type u_1
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type ?u.3145
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x✝ : U → C
hx : HasAdjDiff C x✝
x : U
⊢ CDifferentiableAt C (fun u => exp (x✝ u)) x

case right
R : Type u_3
C : Type u_1
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type ?u.3145
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x✝ : U → C
hx : HasAdjDiff C x✝
x : U
⊢ HasSemiAdjoint C (cderiv C (fun u => exp (x✝ u)) x)
Tactic:
fun_prop
Proof state after:
case right
R : Type u_3
C : Type u_1
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type ?u.3145
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x✝ : U → C
hx : HasAdjDiff C x✝
x : U
⊢ HasSemiAdjoint C (cderiv C (fun u => exp (x✝ u)) x)
Theorem: SciLean.Scalar.exp.arg_x.HasAdjDiff_rule
Proof state before:
case right
R : Type u_3
C : Type u_1
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type ?u.3145
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x✝ : U → C
hx : HasAdjDiff C x✝
x : U
⊢ HasSemiAdjoint C (cderiv C (fun u => exp (x✝ u)) x)
Tactic:
fun_trans [fwdDeriv]
Proof state after:
case right
R : Type u_3
C : Type u_1
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type ?u.3145
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x✝ : U → C
hx : HasAdjDiff C x✝
x : U
⊢ HasSemiAdjoint C fun dw => cderiv C (fun w => x✝ w) x dw * exp (x✝ x)
Theorem: SciLean.Scalar.exp.arg_x.HasAdjDiff_rule
Proof state before:
case right
R : Type u_3
C : Type u_1
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type ?u.3145
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x✝ : U → C
hx : HasAdjDiff C x✝
x : U
⊢ HasSemiAdjoint C fun dw => cderiv C (fun w => x✝ w) x dw * exp (x✝ x)
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.Scalar.exp.arg_x.revDeriv_rule
Proof state before:
R : Type u_3
C : Type u_1
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type ?u.5049
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x : U → C
hx : HasAdjDiff C x
⊢ (revDeriv C fun u => exp (x u)) = fun u =>
    let xdx := revDeriv C x u;
    (exp xdx.1, fun dy => xdx.2 ((starRingEnd C) (exp xdx.1) * dy))
Tactic:
unfold revDeriv
Proof state after:
R : Type u_3
C : Type u_1
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type ?u.5049
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x : U → C
hx : HasAdjDiff C x
⊢ (fun x_1 => ((fun u => exp (x u)) x_1, semiAdjoint C (cderiv C (fun u => exp (x u)) x_1))) = fun u =>
    let xdx := (x u, semiAdjoint C (cderiv C x u));
    (exp xdx.1, fun dy => xdx.2 ((starRingEnd C) (exp xdx.1) * dy))
Theorem: SciLean.Scalar.exp.arg_x.revDeriv_rule
Proof state before:
R : Type u_3
C : Type u_1
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type ?u.5049
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x : U → C
hx : HasAdjDiff C x
⊢ (fun x_1 => ((fun u => exp (x u)) x_1, semiAdjoint C (cderiv C (fun u => exp (x u)) x_1))) = fun u =>
    let xdx := (x u, semiAdjoint C (cderiv C x u));
    (exp xdx.1, fun dy => xdx.2 ((starRingEnd C) (exp xdx.1) * dy))
Tactic:
fun_trans only [fwdDeriv, smul_push, ftrans_simp]
Proof state after:
no goals
Theorem: SciLean.Scalar.log.arg_x.CDifferentiable_rule
Proof state before:
R✝ : Type ?u.7797
C : Type ?u.7796
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.7806
inst✝⁴ : Vec C W✝
U✝ : Type ?u.7829
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.7879
inst✝ : SemiInnerProductSpace R U
x : W → R
hx : CDifferentiable R x
hw : ∀ (w : W), x w ≠ 0
⊢ CDifferentiable R fun w => log (x w)
Tactic:
intro x
Proof state after:
R✝ : Type ?u.7797
C : Type ?u.7796
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.7806
inst✝⁴ : Vec C W✝
U✝ : Type ?u.7829
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.7879
inst✝ : SemiInnerProductSpace R U
x✝ : W → R
hx : CDifferentiable R x✝
hw : ∀ (w : W), x✝ w ≠ 0
x : W
⊢ CDifferentiableAt R (fun w => log (x✝ w)) x
Theorem: SciLean.Scalar.log.arg_x.CDifferentiable_rule
Proof state before:
R✝ : Type ?u.7797
C : Type ?u.7796
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.7806
inst✝⁴ : Vec C W✝
U✝ : Type ?u.7829
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.7879
inst✝ : SemiInnerProductSpace R U
x✝ : W → R
hx : CDifferentiable R x✝
hw : ∀ (w : W), x✝ w ≠ 0
x : W
⊢ CDifferentiableAt R (fun w => log (x✝ w)) x
Tactic:
fun_prop (disch:=aesop)
Proof state after:
no goals
Theorem: SciLean.Scalar.log.arg_x.CDifferentiable_rule
Proof state before:
case funProp.discharger
R✝ : Type ?u.7797
C : Type ?u.7796
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.7806
inst✝⁴ : Vec C W✝
U✝ : Type ?u.7829
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.7879
inst✝ : SemiInnerProductSpace R U
x✝ : W → R
hx : CDifferentiable R x✝
hw : ∀ (w : W), x✝ w ≠ 0
x : W
⊢ x✝ x ≠ 0
Tactic:
aesop
Proof state after:
no goals
Theorem: SciLean.Scalar.log.arg_x.cderiv_rule
Proof state before:
R✝ : Type ?u.10194
C : Type ?u.10193
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.10203
inst✝⁴ : Vec C W✝
U✝ : Type ?u.10226
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.10276
inst✝ : SemiInnerProductSpace R U
x : W → R
hx : CDifferentiable R x
hw : ∀ (w : W), x w ≠ 0
⊢ (cderiv R fun w => log (x w)) = fun w dw =>
    let xdx := fwdDeriv R x w dw;
    xdx.2 / abs xdx.1
Tactic:
funext x
Proof state after:
case h
R✝ : Type ?u.10194
C : Type ?u.10193
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.10203
inst✝⁴ : Vec C W✝
U✝ : Type ?u.10226
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.10276
inst✝ : SemiInnerProductSpace R U
x✝ : W → R
hx : CDifferentiable R x✝
hw : ∀ (w : W), x✝ w ≠ 0
x : W
⊢ cderiv R (fun w => log (x✝ w)) x = fun dw =>
    let xdx := fwdDeriv R x✝ x dw;
    xdx.2 / abs xdx.1
Theorem: SciLean.Scalar.log.arg_x.cderiv_rule
Proof state before:
case h
R✝ : Type ?u.10194
C : Type ?u.10193
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.10203
inst✝⁴ : Vec C W✝
U✝ : Type ?u.10226
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.10276
inst✝ : SemiInnerProductSpace R U
x✝ : W → R
hx : CDifferentiable R x✝
hw : ∀ (w : W), x✝ w ≠ 0
x : W
⊢ cderiv R (fun w => log (x✝ w)) x = fun dw =>
    let xdx := fwdDeriv R x✝ x dw;
    xdx.2 / abs xdx.1
Tactic:
fun_trans (disch:=aesop)
Proof state after:
no goals
Theorem: SciLean.Scalar.log.arg_x.cderiv_rule
Proof state before:
case funProp.discharger
R✝ : Type ?u.10194
C : Type ?u.10193
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.10203
inst✝⁴ : Vec C W✝
U✝ : Type ?u.10226
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.10276
inst✝ : SemiInnerProductSpace R U
x✝ : W → R
hx : CDifferentiable R x✝
hw : ∀ (w : W), x✝ w ≠ 0
x : W
⊢ x✝ x ≠ 0
Tactic:
aesop
Proof state after:
no goals
Theorem: SciLean.Scalar.log.arg_x.fwdDeriv_rule_at
Proof state before:
R✝ : Type ?u.13993
C : Type ?u.13992
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.14002
inst✝⁴ : Vec C W✝
U✝ : Type ?u.14025
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.14075
inst✝ : SemiInnerProductSpace R U
w : W
x : W → R
hx : CDifferentiableAt R x w
hw : x w ≠ 0
⊢ fwdDeriv R (fun w => log (x w)) w = fun dw =>
    let xdx := fwdDeriv R x w dw;
    let l := log xdx.1;
    (l, xdx.2 / abs xdx.1)
Tactic:
unfold fwdDeriv
Proof state after:
R✝ : Type ?u.13993
C : Type ?u.13992
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.14002
inst✝⁴ : Vec C W✝
U✝ : Type ?u.14025
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.14075
inst✝ : SemiInnerProductSpace R U
w : W
x : W → R
hx : CDifferentiableAt R x w
hw : x w ≠ 0
⊢ (fun dx => ((fun w => log (x w)) w, cderiv R (fun w => log (x w)) w dx)) = fun dw =>
    let xdx := (x w, cderiv R x w dw);
    let l := log xdx.1;
    (l, xdx.2 / abs xdx.1)
Theorem: SciLean.Scalar.log.arg_x.fwdDeriv_rule_at
Proof state before:
R✝ : Type ?u.13993
C : Type ?u.13992
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.14002
inst✝⁴ : Vec C W✝
U✝ : Type ?u.14025
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.14075
inst✝ : SemiInnerProductSpace R U
w : W
x : W → R
hx : CDifferentiableAt R x w
hw : x w ≠ 0
⊢ (fun dx => ((fun w => log (x w)) w, cderiv R (fun w => log (x w)) w dx)) = fun dw =>
    let xdx := (x w, cderiv R x w dw);
    let l := log xdx.1;
    (l, xdx.2 / abs xdx.1)
Tactic:
fun_trans (disch:=assumption)
Proof state after:
R✝ : Type ?u.13993
C : Type ?u.13992
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.14002
inst✝⁴ : Vec C W✝
U✝ : Type ?u.14025
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.14075
inst✝ : SemiInnerProductSpace R U
w : W
x : W → R
hx : CDifferentiableAt R x w
hw : x w ≠ 0
⊢ (fun dx => (log (x w), (fwdDeriv R (fun w => x w) w dx).2 / abs (fwdDeriv R (fun w => x w) w dx).1)) = fun dw =>
    (log (x w), cderiv R x w dw / abs (x w))
Theorem: SciLean.Scalar.log.arg_x.fwdDeriv_rule_at
Proof state before:
R✝ : Type ?u.13993
C : Type ?u.13992
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.14002
inst✝⁴ : Vec C W✝
U✝ : Type ?u.14025
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.14075
inst✝ : SemiInnerProductSpace R U
w : W
x : W → R
hx : CDifferentiableAt R x w
hw : x w ≠ 0
⊢ (fun dx => (log (x w), (fwdDeriv R (fun w => x w) w dx).2 / abs (fwdDeriv R (fun w => x w) w dx).1)) = fun dw =>
    (log (x w), cderiv R x w dw / abs (x w))
Tactic:
simp[fwdDeriv]
Proof state after:
no goals
Theorem: SciLean.Scalar.log.arg_x.fwdDeriv_rule_at
Proof state before:
case funProp.discharger
R✝ : Type ?u.13993
C : Type ?u.13992
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.14002
inst✝⁴ : Vec C W✝
U✝ : Type ?u.14025
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.14075
inst✝ : SemiInnerProductSpace R U
w : W
x : W → R
hx : CDifferentiableAt R x w
hw : x w ≠ 0
dx : W
⊢ x w ≠ 0
Tactic:
assumption
Proof state after:
no goals
Theorem: SciLean.Scalar.log.arg_x.fwdDeriv_rule
Proof state before:
R✝ : Type ?u.18049
C : Type ?u.18048
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.18058
inst✝⁴ : Vec C W✝
U✝ : Type ?u.18081
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.18131
inst✝ : SemiInnerProductSpace R U
x : W → R
hx : CDifferentiable R x
hw : ∀ (w : W), x w ≠ 0
⊢ (fwdDeriv R fun w => log (x w)) = fun w dw =>
    let xdx := fwdDeriv R x w dw;
    let l := log xdx.1;
    (l, xdx.2 / abs xdx.1)
Tactic:
unfold fwdDeriv
Proof state after:
R✝ : Type ?u.18049
C : Type ?u.18048
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.18058
inst✝⁴ : Vec C W✝
U✝ : Type ?u.18081
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.18131
inst✝ : SemiInnerProductSpace R U
x : W → R
hx : CDifferentiable R x
hw : ∀ (w : W), x w ≠ 0
⊢ (fun x_1 dx => ((fun w => log (x w)) x_1, cderiv R (fun w => log (x w)) x_1 dx)) = fun w dw =>
    let xdx := (x w, cderiv R x w dw);
    let l := log xdx.1;
    (l, xdx.2 / abs xdx.1)
Theorem: SciLean.Scalar.log.arg_x.fwdDeriv_rule
Proof state before:
R✝ : Type ?u.18049
C : Type ?u.18048
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.18058
inst✝⁴ : Vec C W✝
U✝ : Type ?u.18081
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.18131
inst✝ : SemiInnerProductSpace R U
x : W → R
hx : CDifferentiable R x
hw : ∀ (w : W), x w ≠ 0
⊢ (fun x_1 dx => ((fun w => log (x w)) x_1, cderiv R (fun w => log (x w)) x_1 dx)) = fun w dw =>
    let xdx := (x w, cderiv R x w dw);
    let l := log xdx.1;
    (l, xdx.2 / abs xdx.1)
Tactic:
fun_trans (disch:=assumption)
Proof state after:
R✝ : Type ?u.18049
C : Type ?u.18048
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.18058
inst✝⁴ : Vec C W✝
U✝ : Type ?u.18081
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.18131
inst✝ : SemiInnerProductSpace R U
x : W → R
hx : CDifferentiable R x
hw : ∀ (w : W), x w ≠ 0
⊢ (fun x_1 dx => (log (x x_1), (fwdDeriv R (fun w => x w) x_1 dx).2 / abs (fwdDeriv R (fun w => x w) x_1 dx).1)) =
    fun w dw => (log (x w), cderiv R x w dw / abs (x w))
Theorem: SciLean.Scalar.log.arg_x.fwdDeriv_rule
Proof state before:
R✝ : Type ?u.18049
C : Type ?u.18048
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.18058
inst✝⁴ : Vec C W✝
U✝ : Type ?u.18081
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.18131
inst✝ : SemiInnerProductSpace R U
x : W → R
hx : CDifferentiable R x
hw : ∀ (w : W), x w ≠ 0
⊢ (fun x_1 dx => (log (x x_1), (fwdDeriv R (fun w => x w) x_1 dx).2 / abs (fwdDeriv R (fun w => x w) x_1 dx).1)) =
    fun w dw => (log (x w), cderiv R x w dw / abs (x w))
Tactic:
simp[fwdDeriv]
Proof state after:
no goals
Theorem: SciLean.Scalar.log.arg_x.fwdDeriv_rule
Proof state before:
case funProp.discharger
R✝ : Type ?u.18049
C : Type ?u.18048
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.18058
inst✝⁴ : Vec C W✝
U✝ : Type ?u.18081
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.18131
inst✝ : SemiInnerProductSpace R U
x✝ : W → R
hx : CDifferentiable R x✝
hw : ∀ (w : W), x✝ w ≠ 0
x dx : W
⊢ ∀ (w : W), x✝ w ≠ 0
Tactic:
assumption
Proof state after:
no goals
Theorem: SciLean.Scalar.log.arg_x.HasAdjDiffAt_rule
Proof state before:
R✝ : Type ?u.22335
C : Type ?u.22334
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.22344
inst✝⁴ : Vec C W✝
U✝ : Type ?u.22367
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.22389
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
u : U
x : U → R
hx : HasAdjDiffAt R x u
hu : x u ≠ 0
⊢ HasAdjDiffAt R (fun u => log (x u)) u
Tactic:
constructor
Proof state after:
case left
R✝ : Type ?u.22335
C : Type ?u.22334
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.22344
inst✝⁴ : Vec C W✝
U✝ : Type ?u.22367
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.22389
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
u : U
x : U → R
hx : HasAdjDiffAt R x u
hu : x u ≠ 0
⊢ CDifferentiableAt R (fun u => log (x u)) u

case right
R✝ : Type ?u.22335
C : Type ?u.22334
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.22344
inst✝⁴ : Vec C W✝
U✝ : Type ?u.22367
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.22389
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
u : U
x : U → R
hx : HasAdjDiffAt R x u
hu : x u ≠ 0
⊢ HasSemiAdjoint R (cderiv R (fun u => log (x u)) u)
Theorem: SciLean.Scalar.log.arg_x.HasAdjDiffAt_rule
Proof state before:
case left
R✝ : Type ?u.22335
C : Type ?u.22334
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.22344
inst✝⁴ : Vec C W✝
U✝ : Type ?u.22367
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.22389
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
u : U
x : U → R
hx : HasAdjDiffAt R x u
hu : x u ≠ 0
⊢ CDifferentiableAt R (fun u => log (x u)) u

case right
R✝ : Type ?u.22335
C : Type ?u.22334
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.22344
inst✝⁴ : Vec C W✝
U✝ : Type ?u.22367
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.22389
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
u : U
x : U → R
hx : HasAdjDiffAt R x u
hu : x u ≠ 0
⊢ HasSemiAdjoint R (cderiv R (fun u => log (x u)) u)
Tactic:
fun_prop (disch:=aesop)
Proof state after:
case right
R✝ : Type ?u.22335
C : Type ?u.22334
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.22344
inst✝⁴ : Vec C W✝
U✝ : Type ?u.22367
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.22389
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
u : U
x : U → R
hx : HasAdjDiffAt R x u
hu : x u ≠ 0
⊢ HasSemiAdjoint R (cderiv R (fun u => log (x u)) u)
Theorem: SciLean.Scalar.log.arg_x.HasAdjDiffAt_rule
Proof state before:
case right
R✝ : Type ?u.22335
C : Type ?u.22334
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.22344
inst✝⁴ : Vec C W✝
U✝ : Type ?u.22367
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.22389
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
u : U
x : U → R
hx : HasAdjDiffAt R x u
hu : x u ≠ 0
⊢ HasSemiAdjoint R (cderiv R (fun u => log (x u)) u)
Tactic:
fun_trans (disch:=aesop) [fwdDeriv]
Proof state after:
case right
R✝ : Type ?u.22335
C : Type ?u.22334
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.22344
inst✝⁴ : Vec C W✝
U✝ : Type ?u.22367
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.22389
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
u : U
x : U → R
hx : HasAdjDiffAt R x u
hu : x u ≠ 0
⊢ HasSemiAdjoint R fun dw => cderiv R (fun w => x w) u dw / abs (x u)
Theorem: SciLean.Scalar.log.arg_x.HasAdjDiffAt_rule
Proof state before:
case right
R✝ : Type ?u.22335
C : Type ?u.22334
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.22344
inst✝⁴ : Vec C W✝
U✝ : Type ?u.22367
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.22389
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
u : U
x : U → R
hx : HasAdjDiffAt R x u
hu : x u ≠ 0
⊢ HasSemiAdjoint R fun dw => cderiv R (fun w => x w) u dw / abs (x u)
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.Scalar.log.arg_x.HasAdjDiffAt_rule
Proof state before:
case funProp.discharger
R✝ : Type ?u.22335
C : Type ?u.22334
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.22344
inst✝⁴ : Vec C W✝
U✝ : Type ?u.22367
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.22389
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
u : U
x : U → R
hx : HasAdjDiffAt R x u
hu : x u ≠ 0
⊢ x u ≠ 0
Tactic:
aesop
Proof state after:
no goals
Theorem: SciLean.Scalar.log.arg_x.HasAdjDiff_rule
Proof state before:
R✝ : Type ?u.25096
C : Type ?u.25095
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.25105
inst✝⁴ : Vec C W✝
U✝ : Type ?u.25128
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.25150
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
⊢ HasAdjDiff R fun u => log (x u)
Tactic:
intro u
Proof state after:
R✝ : Type ?u.25096
C : Type ?u.25095
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.25105
inst✝⁴ : Vec C W✝
U✝ : Type ?u.25128
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.25150
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
u : U
⊢ HasAdjDiffAt R (fun u => log (x u)) u
Theorem: SciLean.Scalar.log.arg_x.HasAdjDiff_rule
Proof state before:
R✝ : Type ?u.25096
C : Type ?u.25095
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.25105
inst✝⁴ : Vec C W✝
U✝ : Type ?u.25128
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.25150
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
u : U
⊢ HasAdjDiffAt R (fun u => log (x u)) u
Tactic:
fun_prop (disch:=aesop)
Proof state after:
no goals
Theorem: SciLean.Scalar.log.arg_x.HasAdjDiff_rule
Proof state before:
case funProp.discharger
R✝ : Type ?u.25096
C : Type ?u.25095
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.25105
inst✝⁴ : Vec C W✝
U✝ : Type ?u.25128
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.25150
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
u : U
⊢ x u ≠ 0
Tactic:
aesop
Proof state after:
no goals
Theorem: SciLean.Scalar.log.arg_x.revDeriv_rule_at
Proof state before:
R✝ : Type ?u.26877
C : Type ?u.26876
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.26886
inst✝⁴ : Vec C W✝
U✝ : Type ?u.26909
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.26931
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
u : U
x : U → R
hx : HasAdjDiffAt R x u
hu : x u ≠ 0
⊢ revDeriv R (fun u => log (x u)) u =
    let xdx := revDeriv R x u;
    (log xdx.1, fun dy => xdx.2 ((abs (x u))⁻¹ * dy))
Tactic:
unfold revDeriv
Proof state after:
R✝ : Type ?u.26877
C : Type ?u.26876
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.26886
inst✝⁴ : Vec C W✝
U✝ : Type ?u.26909
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.26931
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
u : U
x : U → R
hx : HasAdjDiffAt R x u
hu : x u ≠ 0
⊢ ((fun u => log (x u)) u, semiAdjoint R (cderiv R (fun u => log (x u)) u)) =
    let xdx := (x u, semiAdjoint R (cderiv R x u));
    (log xdx.1, fun dy => xdx.2 ((abs (x u))⁻¹ * dy))
Theorem: SciLean.Scalar.log.arg_x.revDeriv_rule_at
Proof state before:
R✝ : Type ?u.26877
C : Type ?u.26876
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.26886
inst✝⁴ : Vec C W✝
U✝ : Type ?u.26909
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.26931
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
u : U
x : U → R
hx : HasAdjDiffAt R x u
hu : x u ≠ 0
⊢ ((fun u => log (x u)) u, semiAdjoint R (cderiv R (fun u => log (x u)) 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_at
Proof state before:
case funProp.discharger
R✝ : Type ?u.26877
C : Type ?u.26876
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.26886
inst✝⁴ : Vec C W✝
U✝ : Type ?u.26909
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.26931
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
u : U
x : U → R
hx : HasAdjDiffAt R x u
hu : x u ≠ 0
⊢ x u ≠ 0
Tactic:
aesop
Proof state after:
no goals
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
⊢ (revDeriv R fun u => log (x u)) = fun u =>
    let xdx := revDeriv R x u;
    (log xdx.1, fun dy => xdx.2 ((abs (x u))⁻¹ * dy))
Tactic:
unfold revDeriv
Proof state after:
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))