internlm/Lean-Github huggingface dataset:
Theorem: SciLean.norm₂.arg_x.revDerivProj_rule_at
Proof 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
Proof 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)
Theorem: SciLean.norm₂.arg_x.revDerivProj_rule_at
Proof 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]
Proof state after:
no goals
Theorem: SciLean.norm₂.arg_x.revDerivProj_rule_at
Proof 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
Proof state after:
no goals
Theorem: SciLean.norm₂.arg_x.revDerivProjUpdate_rule_at
Proof 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
⊢ revDerivProjUpdate R Unit (fun x => ‖f x‖₂[R]) x =
    let ydf := revDerivUpdate R f x;
    let ynorm := ‖ydf.1‖₂[R];
    (ynorm, fun x dr dx => ydf.2 ((ynorm⁻¹ * dr) • ydf.1) dx)
Tactic:
have ⟨_,_⟩ := hf
Proof 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
left✝ : CDifferentiableAt R f x
right✝ : HasSemiAdjoint R (cderiv R f x)
⊢ revDerivProjUpdate R Unit (fun x => ‖f x‖₂[R]) x =
    let ydf := revDerivUpdate R f x;
    let ynorm := ‖ydf.1‖₂[R];
    (ynorm, fun x dr dx => ydf.2 ((ynorm⁻¹ * dr) • ydf.1) dx)
Theorem: SciLean.norm₂.arg_x.revDerivProjUpdate_rule_at
Proof 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
left✝ : CDifferentiableAt R f x
right✝ : HasSemiAdjoint R (cderiv R f x)
⊢ revDerivProjUpdate R Unit (fun x => ‖f x‖₂[R]) x =
    let ydf := revDerivUpdate R f x;
    let ynorm := ‖ydf.1‖₂[R];
    (ynorm, fun x dr dx => ydf.2 ((ynorm⁻¹ * dr) • ydf.1) dx)
Tactic:
simp[revDerivProjUpdate]
Proof 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
left✝ : CDifferentiableAt R f x
right✝ : HasSemiAdjoint R (cderiv R f x)
⊢ (fun i de dx => dx + (revDerivProj R Unit (fun x => ‖f x‖₂[R]) x).2 i de) = fun x_1 dr dx =>
    (revDerivUpdate R f x).2 ((‖f x‖₂[R]⁻¹ * dr) • f x) dx
Theorem: SciLean.norm₂.arg_x.revDerivProjUpdate_rule_at
Proof 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
left✝ : CDifferentiableAt R f x
right✝ : HasSemiAdjoint R (cderiv R f x)
⊢ (fun i de dx => dx + (revDerivProj R Unit (fun x => ‖f x‖₂[R]) x).2 i de) = fun x_1 dr dx =>
    (revDerivUpdate R f x).2 ((‖f x‖₂[R]⁻¹ * dr) • f x) dx
Tactic:
fun_trans (disch:=assumption) only
Proof 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
left✝ : CDifferentiableAt R f x
right✝ : HasSemiAdjoint R (cderiv R f x)
⊢ (fun i de dx =>
      dx +
        (‖(revDeriv R (fun x => f x) x).1‖₂[R]⁻¹ * de) •
          (revDeriv R (fun x => f x) x).2 (revDeriv R (fun x => f x) x).1) =
    fun x_1 dr dx => (revDerivUpdate R f x).2 ((‖f x‖₂[R]⁻¹ * dr) • f x) dx
Theorem: SciLean.norm₂.arg_x.revDerivProjUpdate_rule_at
Proof 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
left✝ : CDifferentiableAt R f x
right✝ : HasSemiAdjoint R (cderiv R f x)
⊢ (fun i de dx =>
      dx +
        (‖(revDeriv R (fun x => f x) x).1‖₂[R]⁻¹ * de) •
          (revDeriv R (fun x => f x) x).2 (revDeriv R (fun x => f x) x).1) =
    fun x_1 dr dx => (revDerivUpdate R f x).2 ((‖f x‖₂[R]⁻¹ * dr) • f x) dx
Tactic:
simp[revDeriv,revDerivUpdate,smul_pull]
Proof state after:
no goals
Theorem: SciLean.norm₂.arg_x.revDerivProjUpdate_rule_at
Proof 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
left✝ : CDifferentiableAt R f x
right✝ : HasSemiAdjoint R (cderiv R f x)
i : Unit
de : R
dx : X
⊢ f x ≠ 0
Tactic:
assumption
Proof state after:
no goals
Theorem: SciLean.norm₂.arg_x.revDeriv_rule
Proof 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
hf : HasAdjDiff R f
hx : ∀ (x : X), f x ≠ 0
⊢ (revDeriv R fun x => ‖f x‖₂[R]) = fun x =>
    let ydf := revDeriv R f x;
    let ynorm := ‖ydf.1‖₂[R];
    (ynorm, fun dr => (ynorm⁻¹ * dr) • ydf.2 ydf.1)
Tactic:
unfold revDeriv
Proof 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
hf : HasAdjDiff R f
hx : ∀ (x : X), f x ≠ 0
⊢ (fun x => ((fun x => ‖f x‖₂[R]) x, semiAdjoint R (cderiv R (fun x => ‖f x‖₂[R]) x))) = fun x =>
    let ydf := (f x, semiAdjoint R (cderiv R f x));
    let ynorm := ‖ydf.1‖₂[R];
    (ynorm, fun dr => (ynorm⁻¹ * dr) • ydf.2 ydf.1)