Theorem: SciLean.norm₂.arg_x.revDerivProj_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
⊢ revDerivProj R Unit (fun x => ‖f x‖₂[R]) x =
    let ydf := revDeriv R f x;
    let ynorm := ‖ydf.1‖₂[R];
    (ynorm, fun x dr => (ynorm⁻¹ * dr) • ydf.2 ydf.1)
Tactic:
simp[revDerivProj]
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 i de => (revDeriv R (fun x => ‖f x‖₂[R]) x).2 (oneHot i de)) = fun x_1 dr =>
    (‖f x‖₂[R]⁻¹ * dr) • (revDeriv R f x).2 (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 i de => (revDeriv R (fun x => ‖f x‖₂[R]) x).2 (oneHot i de)) = fun x_1 dr =>
    (‖f x‖₂[R]⁻¹ * dr) • (revDeriv R f x).2 (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 i de =>
      (‖(revDeriv R (fun x => f x) x).1‖₂[R]⁻¹ * oneHot i de) •
        (revDeriv R (fun x => f x) x).2 (revDeriv R (fun x => f x) x).1) =
    fun x_1 dr => (‖f x‖₂[R]⁻¹ * dr) • (revDeriv R f x).2 (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 i de =>
      (‖(revDeriv R (fun x => f x) x).1‖₂[R]⁻¹ * oneHot i de) •
        (revDeriv R (fun x => f x) x).2 (revDeriv R (fun x => f x) x).1) =
    fun x_1 dr => (‖f x‖₂[R]⁻¹ * dr) • (revDeriv R f x).2 (f x)
Tactic:
simp[oneHot, structMake]
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
i : Unit
de : R
⊢ f x ≠ 0
Tactic:
assumption
State after:
no goals