internlm/Lean-Github huggingface dataset:
Theorem: LeanColls.Indexed.ofFn.arg_cont.revCDerivProj_rule
Proof state before:
case h
K : Type
inst✝⁶ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁵ : ArrayType Cont Idx Elem
inst✝⁴ : IndexType Idx
inst✝³ : LawfulIndexType Idx
inst✝² : DecidableEq Idx
X : Type
inst✝¹ : SemiInnerProductSpace K X
inst✝ : SemiInnerProductSpace K Elem
f : X → Idx → Elem
hf : HasAdjDiff K f
x : X
⊢ (ofFn (f x), fun i de => (revDeriv K (fun x => f x) x).2 fun idx => (oneHot i de)[idx]) =
    let fdf :=
      let ydf' := revDeriv K f x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de));
    (ofFn fdf.1, fdf.2)
Tactic:
simp[oneHot]
Proof state after:
no goals
Theorem: LeanColls.Indexed.ofFn.arg_cont.revCDerivProjUpdate_rule
Proof state before:
K : Type
inst✝⁶ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁵ : ArrayType Cont Idx Elem
inst✝⁴ : IndexType Idx
inst✝³ : LawfulIndexType Idx
inst✝² : DecidableEq Idx
X : Type
inst✝¹ : SemiInnerProductSpace K X
inst✝ : SemiInnerProductSpace K Elem
f : X → Idx → Elem
hf : HasAdjDiff K f
⊢ (revDerivProjUpdate K Idx fun x => ofFn (f x)) = fun x =>
    let fdf := revDerivProjUpdate K Idx f x;
    (ofFn fdf.1, fdf.2)
Tactic:
unfold revDerivProjUpdate
Proof state after:
K : Type
inst✝⁶ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁵ : ArrayType Cont Idx Elem
inst✝⁴ : IndexType Idx
inst✝³ : LawfulIndexType Idx
inst✝² : DecidableEq Idx
X : Type
inst✝¹ : SemiInnerProductSpace K X
inst✝ : SemiInnerProductSpace K Elem
f : X → Idx → Elem
hf : HasAdjDiff K f
⊢ (fun x =>
      let ydf' := revDerivProj K Idx (fun x => ofFn (f x)) x;
      (ydf'.1, fun i de dx => dx + ydf'.2 i de)) =
    fun x =>
    let fdf :=
      let ydf' := revDerivProj K Idx f x;
      (ydf'.1, fun i de dx => dx + ydf'.2 i de);
    (ofFn fdf.1, fdf.2)
Theorem: LeanColls.Indexed.ofFn.arg_cont.revCDerivProjUpdate_rule
Proof state before:
K : Type
inst✝⁶ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁵ : ArrayType Cont Idx Elem
inst✝⁴ : IndexType Idx
inst✝³ : LawfulIndexType Idx
inst✝² : DecidableEq Idx
X : Type
inst✝¹ : SemiInnerProductSpace K X
inst✝ : SemiInnerProductSpace K Elem
f : X → Idx → Elem
hf : HasAdjDiff K f
⊢ (fun x =>
      let ydf' := revDerivProj K Idx (fun x => ofFn (f x)) x;
      (ydf'.1, fun i de dx => dx + ydf'.2 i de)) =
    fun x =>
    let fdf :=
      let ydf' := revDerivProj K Idx f x;
      (ydf'.1, fun i de dx => dx + ydf'.2 i de);
    (ofFn fdf.1, fdf.2)
Tactic:
conv => lhs; fun_trans; simp
Proof state after:
no goals
Theorem: SciLean.Scalar.sqrt.arg_x.CDifferentiable_rule
Proof state before:
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.421
inst✝ : SemiInnerProductSpace R U
x : W → R
hx : CDifferentiable R x
hw : ∀ (w : W), x w ≠ 0
⊢ CDifferentiable R fun w => sqrt (x w)
Tactic:
intro x
Proof state after:
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.421
inst✝ : SemiInnerProductSpace R U
x✝ : W → R
hx : CDifferentiable R x✝
hw : ∀ (w : W), x✝ w ≠ 0
x : W
⊢ CDifferentiableAt R (fun w => sqrt (x✝ w)) x
Theorem: SciLean.Scalar.sqrt.arg_x.CDifferentiable_rule
Proof state before:
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.421
inst✝ : SemiInnerProductSpace R U
x✝ : W → R
hx : CDifferentiable R x✝
hw : ∀ (w : W), x✝ w ≠ 0
x : W
⊢ CDifferentiableAt R (fun w => sqrt (x✝ w)) x
Tactic:
fun_prop (disch:=aesop)
Proof state after:
no goals
Theorem: SciLean.Scalar.sqrt.arg_x.CDifferentiable_rule
Proof state before:
case funProp.discharger
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.421
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.sqrt.arg_x.cderiv_rule
Proof state before:
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.3755
inst✝ : SemiInnerProductSpace R U
x : W → R
hx : CDifferentiable R x
hw : ∀ (w : W), 0 < x w
⊢ (cderiv R fun w => sqrt (x w)) = fun w dw =>
    let xdx := fwdDeriv R x w dw;
    xdx.2 / (2 * sqrt xdx.1)
Tactic:
funext x
Proof state after:
case h
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.3755
inst✝ : SemiInnerProductSpace R U
x✝ : W → R
hx : CDifferentiable R x✝
hw : ∀ (w : W), 0 < x✝ w
x : W
⊢ cderiv R (fun w => sqrt (x✝ w)) x = fun dw =>
    let xdx := fwdDeriv R x✝ x dw;
    xdx.2 / (2 * sqrt xdx.1)
Theorem: SciLean.Scalar.sqrt.arg_x.cderiv_rule
Proof state before:
case h
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.3755
inst✝ : SemiInnerProductSpace R U
x✝ : W → R
hx : CDifferentiable R x✝
hw : ∀ (w : W), 0 < x✝ w
x : W
⊢ cderiv R (fun w => sqrt (x✝ w)) x = fun dw =>
    let xdx := fwdDeriv R x✝ x dw;
    xdx.2 / (2 * sqrt xdx.1)
Tactic:
fun_trans (disch:=aesop)
Proof state after:
no goals
Theorem: SciLean.Scalar.sqrt.arg_x.cderiv_rule
Proof state before:
case funProp.discharger
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.3755
inst✝ : SemiInnerProductSpace R U
x✝ : W → R
hx : CDifferentiable R x✝
hw : ∀ (w : W), 0 < x✝ w
x : W
⊢ 0 < x✝ x
Tactic:
aesop
Proof state after:
no goals
Theorem: SciLean.Scalar.sqrt.arg_x.fwdDeriv_rule_at
Proof state before:
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.8937
inst✝ : SemiInnerProductSpace R U
w : W
x : W → R
hx : CDifferentiableAt R x w
hw : 0 < x w
⊢ fwdDeriv R (fun w => sqrt (x w)) w = fun dw =>
    let xdx := fwdDeriv R x w dw;
    let x' := sqrt xdx.1;
    (x', xdx.2 / (2 * x'))
Tactic:
unfold fwdDeriv
Proof state after:
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.8937
inst✝ : SemiInnerProductSpace R U
w : W
x : W → R
hx : CDifferentiableAt R x w
hw : 0 < x w
⊢ (fun dx => ((fun w => sqrt (x w)) w, cderiv R (fun w => sqrt (x w)) w dx)) = fun dw =>
    let xdx := (x w, cderiv R x w dw);
    let x' := sqrt xdx.1;
    (x', xdx.2 / (2 * x'))
Theorem: SciLean.Scalar.sqrt.arg_x.fwdDeriv_rule_at
Proof state before:
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.8937
inst✝ : SemiInnerProductSpace R U
w : W
x : W → R
hx : CDifferentiableAt R x w
hw : 0 < x w
⊢ (fun dx => ((fun w => sqrt (x w)) w, cderiv R (fun w => sqrt (x w)) w dx)) = fun dw =>
    let xdx := (x w, cderiv R x w dw);
    let x' := sqrt xdx.1;
    (x', xdx.2 / (2 * x'))
Tactic:
fun_trans (disch:=assumption) [fwdDeriv]
Proof state after:
no goals
Theorem: SciLean.Scalar.sqrt.arg_x.fwdDeriv_rule_at
Proof state before:
case funProp.discharger
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.8937
inst✝ : SemiInnerProductSpace R U
w : W
x : W → R
hx : CDifferentiableAt R x w
hw : 0 < x w
dx : W
⊢ 0 < x w
Tactic:
assumption
Proof state after:
no goals
Theorem: SciLean.Scalar.sqrt.arg_x.fwdDeriv_rule
Proof state before:
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.13231
inst✝ : SemiInnerProductSpace R U
x : W → R
hx : CDifferentiable R x
hw : ∀ (w : W), 0 < x w
⊢ (fwdDeriv R fun w => sqrt (x w)) = fun w dw =>
    let xdx := fwdDeriv R x w dw;
    let x' := sqrt xdx.1;
    (x', xdx.2 / (2 * x'))
Tactic:
unfold fwdDeriv
Proof state after:
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.13231
inst✝ : SemiInnerProductSpace R U
x : W → R
hx : CDifferentiable R x
hw : ∀ (w : W), 0 < x w
⊢ (fun x_1 dx => ((fun w => sqrt (x w)) x_1, cderiv R (fun w => sqrt (x w)) x_1 dx)) = fun w dw =>
    let xdx := (x w, cderiv R x w dw);
    let x' := sqrt xdx.1;
    (x', xdx.2 / (2 * x'))
Theorem: SciLean.Scalar.sqrt.arg_x.fwdDeriv_rule
Proof state before:
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.13231
inst✝ : SemiInnerProductSpace R U
x : W → R
hx : CDifferentiable R x
hw : ∀ (w : W), 0 < x w
⊢ (fun x_1 dx => ((fun w => sqrt (x w)) x_1, cderiv R (fun w => sqrt (x w)) x_1 dx)) = fun w dw =>
    let xdx := (x w, cderiv R x w dw);
    let x' := sqrt xdx.1;
    (x', xdx.2 / (2 * x'))
Tactic:
fun_trans (disch:=assumption) [fwdDeriv]
Proof state after:
no goals
Theorem: SciLean.Scalar.sqrt.arg_x.fwdDeriv_rule
Proof state before:
case funProp.discharger
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.13231
inst✝ : SemiInnerProductSpace R U
x✝ : W → R
hx : CDifferentiable R x✝
hw : ∀ (w : W), 0 < x✝ w
x dx : W
⊢ ∀ (w : W), 0 < x✝ w
Tactic:
assumption
Proof state after:
no goals
Theorem: SciLean.Scalar.sqrt.arg_x.HasAdjDiffAt_rule
Proof state before:
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.17689
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
u : U
x : U → R
hx : HasAdjDiffAt R x u
hu : 0 < x u
⊢ HasAdjDiffAt R (fun u => sqrt (x u)) u
Tactic:
constructor
Proof state after:
case left
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.17689
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
u : U
x : U → R
hx : HasAdjDiffAt R x u
hu : 0 < x u
⊢ CDifferentiableAt R (fun u => sqrt (x u)) u

case right
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.17689
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
u : U
x : U → R
hx : HasAdjDiffAt R x u
hu : 0 < x u
⊢ HasSemiAdjoint R (cderiv R (fun u => sqrt (x u)) u)
Theorem: SciLean.Scalar.sqrt.arg_x.HasAdjDiffAt_rule
Proof state before:
case left
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.17689
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
u : U
x : U → R
hx : HasAdjDiffAt R x u
hu : 0 < x u
⊢ CDifferentiableAt R (fun u => sqrt (x u)) u

case right
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.17689
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
u : U
x : U → R
hx : HasAdjDiffAt R x u
hu : 0 < x u
⊢ HasSemiAdjoint R (cderiv R (fun u => sqrt (x u)) u)
Tactic:
fun_prop (disch:=aesop)
Proof state after:
case right
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.17689
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
u : U
x : U → R
hx : HasAdjDiffAt R x u
hu : 0 < x u
⊢ HasSemiAdjoint R (cderiv R (fun u => sqrt (x u)) u)
Theorem: SciLean.Scalar.sqrt.arg_x.HasAdjDiffAt_rule
Proof state before:
case right
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.17689
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
u : U
x : U → R
hx : HasAdjDiffAt R x u
hu : 0 < x u
⊢ HasSemiAdjoint R (cderiv R (fun u => sqrt (x u)) u)
Tactic:
fun_trans (disch:=aesop) [fwdDeriv]
Proof state after:
case right
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.17689
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
u : U
x : U → R
hx : HasAdjDiffAt R x u
hu : 0 < x u
⊢ HasSemiAdjoint R fun dw => cderiv R (fun w => x w) u dw / (2 * sqrt (x u))
Theorem: SciLean.Scalar.sqrt.arg_x.HasAdjDiffAt_rule
Proof state before:
case right
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.17689
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
u : U
x : U → R
hx : HasAdjDiffAt R x u
hu : 0 < x u
⊢ HasSemiAdjoint R fun dw => cderiv R (fun w => x w) u dw / (2 * sqrt (x u))
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.Scalar.sqrt.arg_x.HasAdjDiffAt_rule
Proof state before:
case funProp.discharger
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.17689
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
u : U
x : U → R
hx : HasAdjDiffAt R x u
hu : 0 < x u
⊢ x u ≠ 0
Tactic:
aesop
Proof state after:
no goals
Theorem: SciLean.Scalar.sqrt.arg_x.HasAdjDiffAt_rule
Proof state before:
case funProp.discharger
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.17689
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
u : U
x : U → R
hx : HasAdjDiffAt R x u
hu : 0 < x u
⊢ 0 < x u
Tactic:
aesop
Proof state after:
no goals
Theorem: SciLean.Scalar.sqrt.arg_x.HasAdjDiff_rule
Proof state before:
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.23860
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
x : U → R
hx : HasAdjDiff R x
hu : ∀ (u : U), 0 < x u
⊢ HasAdjDiff R fun u => sqrt (x u)
Tactic:
intro u
Proof state after:
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.23860
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
x : U → R
hx : HasAdjDiff R x
hu : ∀ (u : U), 0 < x u
u : U
⊢ HasAdjDiffAt R (fun u => sqrt (x u)) u
Theorem: SciLean.Scalar.sqrt.arg_x.HasAdjDiff_rule
Proof state before:
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.23860
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
x : U → R
hx : HasAdjDiff R x
hu : ∀ (u : U), 0 < x u
u : U
⊢ HasAdjDiffAt R (fun u => sqrt (x u)) u
Tactic:
fun_prop (disch:=aesop)
Proof state after:
no goals
Theorem: SciLean.Scalar.sqrt.arg_x.HasAdjDiff_rule
Proof state before:
case funProp.discharger
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.23860
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
x : U → R
hx : HasAdjDiff R x
hu : ∀ (u : U), 0 < x u
u : U
⊢ 0 < x u
Tactic:
aesop
Proof state after:
no goals
Theorem: SciLean.Scalar.sqrt.arg_x.revDeriv_rule_at
Proof state before:
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.26483
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
u : U
x : U → R
hx : HasAdjDiffAt R x u
hu : 0 < x u
⊢ revDeriv R (fun u => sqrt (x u)) u =
    let xdx := revDeriv R x u;
    let x' := sqrt xdx.1;
    (x', fun dy => xdx.2 (dy / (2 * x')))
Tactic:
unfold revDeriv
Proof state after:
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.26483
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
u : U
x : U → R
hx : HasAdjDiffAt R x u
hu : 0 < x u
⊢ ((fun u => sqrt (x u)) u, semiAdjoint R (cderiv R (fun u => sqrt (x u)) u)) =
    let xdx := (x u, semiAdjoint R (cderiv R x u));
    let x' := sqrt xdx.1;
    (x', fun dy => xdx.2 (dy / (2 * x')))
Theorem: SciLean.Scalar.sqrt.arg_x.revDeriv_rule_at
Proof state before:
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.26483
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
u : U
x : U → R
hx : HasAdjDiffAt R x u
hu : 0 < x u
⊢ ((fun u => sqrt (x u)) u, semiAdjoint R (cderiv R (fun u => sqrt (x u)) u)) =
    let xdx := (x u, semiAdjoint R (cderiv R x u));
    let x' := sqrt xdx.1;
    (x', fun dy => xdx.2 (dy / (2 * x')))
Tactic:
fun_trans (disch:=aesop) only [fwdDeriv, smul_push, ftrans_simp]
Proof state after:
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.26483
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
u : U
x : U → R
hx : HasAdjDiffAt R x u
hu : 0 < x u
⊢ (sqrt (x u), fun y => semiAdjoint R (fun x_1 => cderiv R (fun w => x w) u x_1) ((2 * sqrt (x u))⁻¹ * y)) =
    (sqrt (x u), fun dy => semiAdjoint R (cderiv R x u) (dy / (2 * sqrt (x u))))
Theorem: SciLean.Scalar.sqrt.arg_x.revDeriv_rule_at
Proof state before:
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.26483
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
u : U
x : U → R
hx : HasAdjDiffAt R x u
hu : 0 < x u
⊢ (sqrt (x u), fun y => semiAdjoint R (fun x_1 => cderiv R (fun w => x w) u x_1) ((2 * sqrt (x u))⁻¹ * y)) =
    (sqrt (x u), fun dy => semiAdjoint R (cderiv R x u) (dy / (2 * sqrt (x u))))
Tactic:
simp
Proof state after:
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.26483
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
u : U
x : U → R
hx : HasAdjDiffAt R x u
hu : 0 < x u
⊢ (fun y => semiAdjoint R (fun x_1 => cderiv R (fun w => x w) u x_1) ((sqrt (x u))⁻¹ * 2⁻¹ * y)) = fun dy =>
    semiAdjoint R (cderiv R x u) (dy / (2 * sqrt (x u)))
Theorem: SciLean.Scalar.sqrt.arg_x.revDeriv_rule_at
Proof state before:
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.26483
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
u : U
x : U → R
hx : HasAdjDiffAt R x u
hu : 0 < x u
⊢ (fun y => semiAdjoint R (fun x_1 => cderiv R (fun w => x w) u x_1) ((sqrt (x u))⁻¹ * 2⁻¹ * y)) = fun dy =>
    semiAdjoint R (cderiv R x u) (dy / (2 * sqrt (x u)))
Tactic:
funext dy
Proof state after:
case h
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.26483
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
u : U
x : U → R
hx : HasAdjDiffAt R x u
hu : 0 < x u
dy : R
⊢ semiAdjoint R (fun x_1 => cderiv R (fun w => x w) u x_1) ((sqrt (x u))⁻¹ * 2⁻¹ * dy) =
    semiAdjoint R (cderiv R x u) (dy / (2 * sqrt (x u)))
Theorem: SciLean.Scalar.sqrt.arg_x.revDeriv_rule_at
Proof state before:
case h
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.26483
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
u : U
x : U → R
hx : HasAdjDiffAt R x u
hu : 0 < x u
dy : R
⊢ semiAdjoint R (fun x_1 => cderiv R (fun w => x w) u x_1) ((sqrt (x u))⁻¹ * 2⁻¹ * dy) =
    semiAdjoint R (cderiv R x u) (dy / (2 * sqrt (x u)))
Tactic:
congr
Proof state after:
case h.e_y
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.26483
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
u : U
x : U → R
hx : HasAdjDiffAt R x u
hu : 0 < x u
dy : R
⊢ (sqrt (x u))⁻¹ * 2⁻¹ * dy = dy / (2 * sqrt (x u))
Theorem: SciLean.Scalar.sqrt.arg_x.revDeriv_rule_at
Proof state before:
case h.e_y
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.26483
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
u : U
x : U → R
hx : HasAdjDiffAt R x u
hu : 0 < x u
dy : R
⊢ (sqrt (x u))⁻¹ * 2⁻¹ * dy = dy / (2 * sqrt (x u))
Tactic:
field_simp [mul_comm]
Proof state after:
no goals
Theorem: SciLean.Scalar.sqrt.arg_x.revDeriv_rule_at
Proof state before:
case funProp.discharger
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.26483
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
u : U
x : U → R
hx : HasAdjDiffAt R x u
hu : 0 < x u
⊢ 0 < x u
Tactic:
aesop
Proof state after:
no goals
Theorem: SciLean.Scalar.sqrt.arg_x.revDeriv_rule
Proof state before:
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.50858
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
x : U → R
hx : HasAdjDiff R x
hu : ∀ (u : U), 0 < x u
⊢ (revDeriv R fun u => sqrt (x u)) = fun u =>
    let xdx := revDeriv R x u;
    let x' := sqrt xdx.1;
    (x', fun dy => xdx.2 (dy / (2 * x')))
Tactic:
funext u
Proof state after:
case h
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.50858
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
x : U → R
hx : HasAdjDiff R x
hu : ∀ (u : U), 0 < x u
u : U
⊢ revDeriv R (fun u => sqrt (x u)) u =
    let xdx := revDeriv R x u;
    let x' := sqrt xdx.1;
    (x', fun dy => xdx.2 (dy / (2 * x')))
Theorem: SciLean.Scalar.sqrt.arg_x.revDeriv_rule
Proof state before:
case h
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.50858
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
x : U → R
hx : HasAdjDiff R x
hu : ∀ (u : U), 0 < x u
u : U
⊢ revDeriv R (fun u => sqrt (x u)) u =
    let xdx := revDeriv R x u;
    let x' := sqrt xdx.1;
    (x', fun dy => xdx.2 (dy / (2 * x')))
Tactic:
fun_trans (disch:=aesop) only [fwdDeriv, smul_push, ftrans_simp]
Proof state after:
no goals
Theorem: SciLean.Scalar.sqrt.arg_x.revDeriv_rule
Proof state before:
case funProp.discharger
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.50858
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
x : U → R
hx : HasAdjDiff R x
hu : ∀ (u : U), 0 < x u
u : U
⊢ 0 < x u
Tactic:
aesop
Proof state after:
no goals
Theorem: SciLean.parametric_inverse_bijection
Proof state before:
R : Type ?u.275
inst✝¹ : RealScalar R
X Y : Type
inst✝ : Nonempty X
f : X → Y
hf : Function.Bijective f
y : Y
⊢ ParametricInverseAt f y (fun x x x => x) (fun x x => Function.invFun f y) fun x => univ
Tactic:
intro i x _
Proof state after:
R : Type ?u.275
inst✝¹ : RealScalar R
X Y : Type
inst✝ : Nonempty X
f : X → Y
hf : Function.Bijective f
y : Y
i x : Unit
a✝ : x ∈ (fun x => univ) i
⊢ f ((fun x x x => x) i x ((fun x x => Function.invFun f y) i x)) = y
Theorem: SciLean.parametric_inverse_bijection
Proof state before:
R : Type ?u.275
inst✝¹ : RealScalar R
X Y : Type
inst✝ : Nonempty X
f : X → Y
hf : Function.Bijective f
y : Y
i x : Unit
a✝ : x ∈ (fun x => univ) i
⊢ f ((fun x x x => x) i x ((fun x x => Function.invFun f y) i x)) = y
Tactic:
simp only
Proof state after:
R : Type ?u.275
inst✝¹ : RealScalar R
X Y : Type
inst✝ : Nonempty X
f : X → Y
hf : Function.Bijective f
y : Y
i x : Unit
a✝ : x ∈ (fun x => univ) i
⊢ f (Function.invFun f y) = y
Theorem: SciLean.parametric_inverse_bijection
Proof state before:
R : Type ?u.275
inst✝¹ : RealScalar R
X Y : Type
inst✝ : Nonempty X
f : X → Y
hf : Function.Bijective f
y : Y
i x : Unit
a✝ : x ∈ (fun x => univ) i
⊢ f (Function.invFun f y) = y
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Prob.randDeriv_const
Proof state before:
R : Type ?u.4672
inst✝¹⁸ : RealScalar R
W : Type u_1
inst✝¹⁷ : NormedAddCommGroup W
inst✝¹⁶ : NormedSpace ℝ W
inst✝¹⁵ : NormedSpace R W
inst✝¹⁴ : MeasurableSpace W
X : Type ?u.4928
inst✝¹³ : NormedAddCommGroup X
inst✝¹² : NormedSpace ℝ X
inst✝¹¹ : NormedSpace R W
inst✝¹⁰ : MeasurableSpace X
Y : Type ?u.5167
inst✝⁹ : NormedAddCommGroup Y
inst✝⁸ : NormedSpace ℝ Y
inst✝⁷ : NormedSpace R W
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.5406
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : NormedSpace R W
inst✝² : MeasurableSpace Z
α : Type
inst✝¹ : MeasurableSpace α
β : Type ?u.5651
inst✝ : MeasurableSpace β
a : Rand α
⊢ (randDeriv fun x => a) = fun w dw => 0
Tactic:
funext w dw
Proof state after:
case h.h
R : Type ?u.4672
inst✝¹⁸ : RealScalar R
W : Type u_1
inst✝¹⁷ : NormedAddCommGroup W
inst✝¹⁶ : NormedSpace ℝ W
inst✝¹⁵ : NormedSpace R W
inst✝¹⁴ : MeasurableSpace W
X : Type ?u.4928
inst✝¹³ : NormedAddCommGroup X
inst✝¹² : NormedSpace ℝ X
inst✝¹¹ : NormedSpace R W
inst✝¹⁰ : MeasurableSpace X
Y : Type ?u.5167
inst✝⁹ : NormedAddCommGroup Y
inst✝⁸ : NormedSpace ℝ Y
inst✝⁷ : NormedSpace R W
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.5406
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : NormedSpace R W
inst✝² : MeasurableSpace Z
α : Type
inst✝¹ : MeasurableSpace α
β : Type ?u.5651
inst✝ : MeasurableSpace β
a : Rand α
w dw : W
⊢ randDeriv (fun x => a) w dw = 0
Theorem: SciLean.Prob.randDeriv_const
Proof state before:
case h.h
R : Type ?u.4672
inst✝¹⁸ : RealScalar R
W : Type u_1
inst✝¹⁷ : NormedAddCommGroup W
inst✝¹⁶ : NormedSpace ℝ W
inst✝¹⁵ : NormedSpace R W
inst✝¹⁴ : MeasurableSpace W
X : Type ?u.4928
inst✝¹³ : NormedAddCommGroup X
inst✝¹² : NormedSpace ℝ X
inst✝¹¹ : NormedSpace R W
inst✝¹⁰ : MeasurableSpace X
Y : Type ?u.5167
inst✝⁹ : NormedAddCommGroup Y
inst✝⁸ : NormedSpace ℝ Y
inst✝⁷ : NormedSpace R W
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.5406
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : NormedSpace R W
inst✝² : MeasurableSpace Z
α : Type
inst✝¹ : MeasurableSpace α
β : Type ?u.5651
inst✝ : MeasurableSpace β
a : Rand α
w dw : W
⊢ randDeriv (fun x => a) w dw = 0
Tactic:
apply DRand.ext
Proof state after:
case h.h.a
R : Type ?u.4672
inst✝¹⁸ : RealScalar R
W : Type u_1
inst✝¹⁷ : NormedAddCommGroup W
inst✝¹⁶ : NormedSpace ℝ W
inst✝¹⁵ : NormedSpace R W
inst✝¹⁴ : MeasurableSpace W
X : Type ?u.4928
inst✝¹³ : NormedAddCommGroup X
inst✝¹² : NormedSpace ℝ X
inst✝¹¹ : NormedSpace R W
inst✝¹⁰ : MeasurableSpace X
Y : Type ?u.5167
inst✝⁹ : NormedAddCommGroup Y
inst✝⁸ : NormedSpace ℝ Y
inst✝⁷ : NormedSpace R W
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.5406
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : NormedSpace R W
inst✝² : MeasurableSpace Z
α : Type
inst✝¹ : MeasurableSpace α
β : Type ?u.5651
inst✝ : MeasurableSpace β
a : Rand α
w dw : W
⊢ ∀ (φ : α → ℝ), (randDeriv (fun x => a) w dw).action φ = 0.action φ