Theorem: SciLean.norm₂.arg_x.revDeriv_rule_at (SciLean/Core/FunctionTransformations/RevDeriv.lean)

State before:
K : Type
inst✝³⁰ : RCLike K
X✝ : Type
inst✝²⁹ : SemiInnerProductSpace K X✝
Y✝ : Type
inst✝²⁸ : SemiInnerProductSpace K Y✝
Z : Type
inst✝²⁷ : SemiInnerProductSpace K Z
X' Xi : Type
XI : Xi → Type
inst✝²⁶ : StructType X' Xi XI
inst✝²⁵ : IndexType Xi
inst✝²⁴ : LawfulIndexType Xi
inst✝²³ : DecidableEq Xi
Y' Yi : Type
YI : Yi → Type
inst✝²² : StructType Y' Yi YI
inst✝²¹ : IndexType Yi
inst✝²⁰ : LawfulIndexType Yi
inst✝¹⁹ : DecidableEq Yi
Z' Zi : Type
ZI : Zi → Type
inst✝¹⁸ : StructType Z' Zi ZI
inst✝¹⁷ : IndexType Zi
inst✝¹⁶ : LawfulIndexType Zi
inst✝¹⁵ : DecidableEq Zi
inst✝¹⁴ : SemiInnerProductSpace K X'
inst✝¹³ : (i : Xi) → SemiInnerProductSpace K (XI i)
inst✝¹² : SemiInnerProductSpaceStruct K X' Xi XI
inst✝¹¹ : SemiInnerProductSpace K Y'
inst✝¹⁰ : (i : Yi) → SemiInnerProductSpace K (YI i)
inst✝⁹ : SemiInnerProductSpaceStruct K Y' Yi YI
inst✝⁸ : SemiInnerProductSpace K Z'
inst✝⁷ : (i : Zi) → SemiInnerProductSpace K (ZI i)
inst✝⁶ : SemiInnerProductSpaceStruct K Z' Zi ZI
W : Type
inst✝⁵ : SemiInnerProductSpace K W
ι : Type
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : SemiInnerProductSpace R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
x : X
hf : HasAdjDiffAt R f x
hx : f x ≠ 0
⊢ revDeriv R (fun x => ‖f x‖₂[R]) x =
    let ydf := revDeriv R f x;
    let ynorm := ‖ydf.1‖₂[R];
    (ynorm, fun dr => (ynorm⁻¹ * dr) • ydf.2 ydf.1)
Tactic:
simp[revDeriv]
State after:
K : Type
inst✝³⁰ : RCLike K
X✝ : Type
inst✝²⁹ : SemiInnerProductSpace K X✝
Y✝ : Type
inst✝²⁸ : SemiInnerProductSpace K Y✝
Z : Type
inst✝²⁷ : SemiInnerProductSpace K Z
X' Xi : Type
XI : Xi → Type
inst✝²⁶ : StructType X' Xi XI
inst✝²⁵ : IndexType Xi
inst✝²⁴ : LawfulIndexType Xi
inst✝²³ : DecidableEq Xi
Y' Yi : Type
YI : Yi → Type
inst✝²² : StructType Y' Yi YI
inst✝²¹ : IndexType Yi
inst✝²⁰ : LawfulIndexType Yi
inst✝¹⁹ : DecidableEq Yi
Z' Zi : Type
ZI : Zi → Type
inst✝¹⁸ : StructType Z' Zi ZI
inst✝¹⁷ : IndexType Zi
inst✝¹⁶ : LawfulIndexType Zi
inst✝¹⁵ : DecidableEq Zi
inst✝¹⁴ : SemiInnerProductSpace K X'
inst✝¹³ : (i : Xi) → SemiInnerProductSpace K (XI i)
inst✝¹² : SemiInnerProductSpaceStruct K X' Xi XI
inst✝¹¹ : SemiInnerProductSpace K Y'
inst✝¹⁰ : (i : Yi) → SemiInnerProductSpace K (YI i)
inst✝⁹ : SemiInnerProductSpaceStruct K Y' Yi YI
inst✝⁸ : SemiInnerProductSpace K Z'
inst✝⁷ : (i : Zi) → SemiInnerProductSpace K (ZI i)
inst✝⁶ : SemiInnerProductSpaceStruct K Z' Zi ZI
W : Type
inst✝⁵ : SemiInnerProductSpace K W
ι : Type
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : SemiInnerProductSpace R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
x : X
hf : HasAdjDiffAt R f x
hx : f x ≠ 0
⊢ semiAdjoint R (cderiv R (fun x => ‖f x‖₂[R]) x) = fun dr => (‖f x‖₂[R]⁻¹ * dr) • semiAdjoint R (cderiv R f x) (f x)

State before:
K : Type
inst✝³⁰ : RCLike K
X✝ : Type
inst✝²⁹ : SemiInnerProductSpace K X✝
Y✝ : Type
inst✝²⁸ : SemiInnerProductSpace K Y✝
Z : Type
inst✝²⁷ : SemiInnerProductSpace K Z
X' Xi : Type
XI : Xi → Type
inst✝²⁶ : StructType X' Xi XI
inst✝²⁵ : IndexType Xi
inst✝²⁴ : LawfulIndexType Xi
inst✝²³ : DecidableEq Xi
Y' Yi : Type
YI : Yi → Type
inst✝²² : StructType Y' Yi YI
inst✝²¹ : IndexType Yi
inst✝²⁰ : LawfulIndexType Yi
inst✝¹⁹ : DecidableEq Yi
Z' Zi : Type
ZI : Zi → Type
inst✝¹⁸ : StructType Z' Zi ZI
inst✝¹⁷ : IndexType Zi
inst✝¹⁶ : LawfulIndexType Zi
inst✝¹⁵ : DecidableEq Zi
inst✝¹⁴ : SemiInnerProductSpace K X'
inst✝¹³ : (i : Xi) → SemiInnerProductSpace K (XI i)
inst✝¹² : SemiInnerProductSpaceStruct K X' Xi XI
inst✝¹¹ : SemiInnerProductSpace K Y'
inst✝¹⁰ : (i : Yi) → SemiInnerProductSpace K (YI i)
inst✝⁹ : SemiInnerProductSpaceStruct K Y' Yi YI
inst✝⁸ : SemiInnerProductSpace K Z'
inst✝⁷ : (i : Zi) → SemiInnerProductSpace K (ZI i)
inst✝⁶ : SemiInnerProductSpaceStruct K Z' Zi ZI
W : Type
inst✝⁵ : SemiInnerProductSpace K W
ι : Type
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : SemiInnerProductSpace R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
x : X
hf : HasAdjDiffAt R f x
hx : f x ≠ 0
⊢ semiAdjoint R (cderiv R (fun x => ‖f x‖₂[R]) x) = fun dr => (‖f x‖₂[R]⁻¹ * dr) • semiAdjoint R (cderiv R f x) (f x)
Tactic:
fun_trans (disch:=assumption) only
State after:
K : Type
inst✝³⁰ : RCLike K
X✝ : Type
inst✝²⁹ : SemiInnerProductSpace K X✝
Y✝ : Type
inst✝²⁸ : SemiInnerProductSpace K Y✝
Z : Type
inst✝²⁷ : SemiInnerProductSpace K Z
X' Xi : Type
XI : Xi → Type
inst✝²⁶ : StructType X' Xi XI
inst✝²⁵ : IndexType Xi
inst✝²⁴ : LawfulIndexType Xi
inst✝²³ : DecidableEq Xi
Y' Yi : Type
YI : Yi → Type
inst✝²² : StructType Y' Yi YI
inst✝²¹ : IndexType Yi
inst✝²⁰ : LawfulIndexType Yi
inst✝¹⁹ : DecidableEq Yi
Z' Zi : Type
ZI : Zi → Type
inst✝¹⁸ : StructType Z' Zi ZI
inst✝¹⁷ : IndexType Zi
inst✝¹⁶ : LawfulIndexType Zi
inst✝¹⁵ : DecidableEq Zi
inst✝¹⁴ : SemiInnerProductSpace K X'
inst✝¹³ : (i : Xi) → SemiInnerProductSpace K (XI i)
inst✝¹² : SemiInnerProductSpaceStruct K X' Xi XI
inst✝¹¹ : SemiInnerProductSpace K Y'
inst✝¹⁰ : (i : Yi) → SemiInnerProductSpace K (YI i)
inst✝⁹ : SemiInnerProductSpaceStruct K Y' Yi YI
inst✝⁸ : SemiInnerProductSpace K Z'
inst✝⁷ : (i : Zi) → SemiInnerProductSpace K (ZI i)
inst✝⁶ : SemiInnerProductSpaceStruct K Z' Zi ZI
W : Type
inst✝⁵ : SemiInnerProductSpace K W
ι : Type
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : SemiInnerProductSpace R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
x : X
hf : HasAdjDiffAt R f x
hx : f x ≠ 0
⊢ (fun y =>
      (starRingEnd R) ‖f x‖₂[R]⁻¹ •
        (starRingEnd R) y • semiAdjoint R (fun x_1 => cderiv R (fun x => f x) x x_1) (f x)) =
    fun dr => (‖f x‖₂[R]⁻¹ * dr) • semiAdjoint R (cderiv R f x) (f x)

State before:
K : Type
inst✝³⁰ : RCLike K
X✝ : Type
inst✝²⁹ : SemiInnerProductSpace K X✝
Y✝ : Type
inst✝²⁸ : SemiInnerProductSpace K Y✝
Z : Type
inst✝²⁷ : SemiInnerProductSpace K Z
X' Xi : Type
XI : Xi → Type
inst✝²⁶ : StructType X' Xi XI
inst✝²⁵ : IndexType Xi
inst✝²⁴ : LawfulIndexType Xi
inst✝²³ : DecidableEq Xi
Y' Yi : Type
YI : Yi → Type
inst✝²² : StructType Y' Yi YI
inst✝²¹ : IndexType Yi
inst✝²⁰ : LawfulIndexType Yi
inst✝¹⁹ : DecidableEq Yi
Z' Zi : Type
ZI : Zi → Type
inst✝¹⁸ : StructType Z' Zi ZI
inst✝¹⁷ : IndexType Zi
inst✝¹⁶ : LawfulIndexType Zi
inst✝¹⁵ : DecidableEq Zi
inst✝¹⁴ : SemiInnerProductSpace K X'
inst✝¹³ : (i : Xi) → SemiInnerProductSpace K (XI i)
inst✝¹² : SemiInnerProductSpaceStruct K X' Xi XI
inst✝¹¹ : SemiInnerProductSpace K Y'
inst✝¹⁰ : (i : Yi) → SemiInnerProductSpace K (YI i)
inst✝⁹ : SemiInnerProductSpaceStruct K Y' Yi YI
inst✝⁸ : SemiInnerProductSpace K Z'
inst✝⁷ : (i : Zi) → SemiInnerProductSpace K (ZI i)
inst✝⁶ : SemiInnerProductSpaceStruct K Z' Zi ZI
W : Type
inst✝⁵ : SemiInnerProductSpace K W
ι : Type
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : SemiInnerProductSpace R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
x : X
hf : HasAdjDiffAt R f x
hx : f x ≠ 0
⊢ (fun y =>
      (starRingEnd R) ‖f x‖₂[R]⁻¹ •
        (starRingEnd R) y • semiAdjoint R (fun x_1 => cderiv R (fun x => f x) x x_1) (f x)) =
    fun dr => (‖f x‖₂[R]⁻¹ * dr) • semiAdjoint R (cderiv R f x) (f x)
Tactic:
simp[smul_smul]
State after:
no goals

State before:
case funProp.discharger
K : Type
inst✝³⁰ : RCLike K
X✝ : Type
inst✝²⁹ : SemiInnerProductSpace K X✝
Y✝ : Type
inst✝²⁸ : SemiInnerProductSpace K Y✝
Z : Type
inst✝²⁷ : SemiInnerProductSpace K Z
X' Xi : Type
XI : Xi → Type
inst✝²⁶ : StructType X' Xi XI
inst✝²⁵ : IndexType Xi
inst✝²⁴ : LawfulIndexType Xi
inst✝²³ : DecidableEq Xi
Y' Yi : Type
YI : Yi → Type
inst✝²² : StructType Y' Yi YI
inst✝²¹ : IndexType Yi
inst✝²⁰ : LawfulIndexType Yi
inst✝¹⁹ : DecidableEq Yi
Z' Zi : Type
ZI : Zi → Type
inst✝¹⁸ : StructType Z' Zi ZI
inst✝¹⁷ : IndexType Zi
inst✝¹⁶ : LawfulIndexType Zi
inst✝¹⁵ : DecidableEq Zi
inst✝¹⁴ : SemiInnerProductSpace K X'
inst✝¹³ : (i : Xi) → SemiInnerProductSpace K (XI i)
inst✝¹² : SemiInnerProductSpaceStruct K X' Xi XI
inst✝¹¹ : SemiInnerProductSpace K Y'
inst✝¹⁰ : (i : Yi) → SemiInnerProductSpace K (YI i)
inst✝⁹ : SemiInnerProductSpaceStruct K Y' Yi YI
inst✝⁸ : SemiInnerProductSpace K Z'
inst✝⁷ : (i : Zi) → SemiInnerProductSpace K (ZI i)
inst✝⁶ : SemiInnerProductSpaceStruct K Z' Zi ZI
W : Type
inst✝⁵ : SemiInnerProductSpace K W
ι : Type
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : SemiInnerProductSpace R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
x : X
hf : HasAdjDiffAt R f x
hx : f x ≠ 0
⊢ f x ≠ 0
Tactic:
assumption
State after:
no goals