Theorem: SciLean.Scalar.log.arg_x.HasAdjDiffAt_rule (SciLean/Core/Functions/Exp.lean)

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
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)

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)
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)

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]
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)

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
State after:
no goals

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
State after:
no goals