internlm/Lean-Github huggingface dataset:
Theorem: SciLean.ArrayType.smul_ofFn
Proof state before:
case a
Cont : Type u_3
Idx : outParam (Type u_4)
Elem : outParam (Type u_2)
inst✝⁴ : IndexType Idx
inst✝³ : outParam (DecidableEq Idx)
inst✝² : LawfulIndexType Idx
inst✝¹ : ArrayType Cont Idx Elem
K : Type u_1
inst✝ : SMul K Elem
f : Idx → Elem
a : K
⊢ ∀ (i : Idx), (a • Indexed.ofFn f)[i] = (Indexed.ofFn fun i => a • f i)[i]
Tactic:
simp[HSMul.hSMul, SMul.smul]
Proof state after:
no goals
Theorem: SciLean.ArrayType.add_get
Proof state before:
Cont : Type u_2
Idx : outParam (Type u_3)
Elem : outParam (Type u_1)
inst✝⁴ : IndexType Idx
inst✝³ : outParam (DecidableEq Idx)
inst✝² : LawfulIndexType Idx
inst✝¹ : ArrayType Cont Idx Elem
inst✝ : Add Elem
x y : Cont
i : Idx
⊢ (x + y)[i] = x[i] + y[i]
Tactic:
simp[HAdd.hAdd,Add.add]
Proof state after:
no goals
Theorem: SciLean.ArrayType.sub_get
Proof state before:
Cont : Type u_2
Idx : outParam (Type u_3)
Elem : outParam (Type u_1)
inst✝⁴ : IndexType Idx
inst✝³ : outParam (DecidableEq Idx)
inst✝² : LawfulIndexType Idx
inst✝¹ : ArrayType Cont Idx Elem
inst✝ : Sub Elem
x y : Cont
i : Idx
⊢ (x - y)[i] = x[i] - y[i]
Tactic:
simp[HSub.hSub,Sub.sub]
Proof state after:
no goals
Theorem: SciLean.ArrayType.mul_get
Proof state before:
Cont : Type u_2
Idx : outParam (Type u_3)
Elem : outParam (Type u_1)
inst✝⁴ : IndexType Idx
inst✝³ : outParam (DecidableEq Idx)
inst✝² : LawfulIndexType Idx
inst✝¹ : ArrayType Cont Idx Elem
inst✝ : Mul Elem
x y : Cont
i : Idx
⊢ (x * y)[i] = x[i] * y[i]
Tactic:
simp[HMul.hMul,Mul.mul]
Proof state after:
no goals
Theorem: SciLean.ArrayType.div_get
Proof state before:
Cont : Type u_2
Idx : outParam (Type u_3)
Elem : outParam (Type u_1)
inst✝⁴ : IndexType Idx
inst✝³ : outParam (DecidableEq Idx)
inst✝² : LawfulIndexType Idx
inst✝¹ : ArrayType Cont Idx Elem
inst✝ : Div Elem
x y : Cont
i : Idx
⊢ (x / y)[i] = x[i] / y[i]
Tactic:
simp[HDiv.hDiv,Div.div]
Proof state after:
no goals
Theorem: SciLean.ArrayType.smul_get
Proof state before:
Cont : Type u_3
Idx : outParam (Type u_4)
Elem : outParam (Type u_2)
inst✝⁴ : IndexType Idx
inst✝³ : outParam (DecidableEq Idx)
inst✝² : LawfulIndexType Idx
inst✝¹ : ArrayType Cont Idx Elem
R : Type u_1
inst✝ : SMul R Elem
r : R
x : Cont
i : Idx
⊢ (r • x)[i] = r • x[i]
Tactic:
simp[HSMul.hSMul,SMul.smul]
Proof state after:
no goals
Theorem: SciLean.ArrayType.neg_get
Proof state before:
Cont : Type u_2
Idx : outParam (Type u_3)
Elem : outParam (Type u_1)
inst✝⁴ : IndexType Idx
inst✝³ : outParam (DecidableEq Idx)
inst✝² : LawfulIndexType Idx
inst✝¹ : ArrayType Cont Idx Elem
inst✝ : Neg Elem
x : Cont
i : Idx
⊢ (-x)[i] = -x[i]
Tactic:
simp[Neg.neg]
Proof state after:
no goals
Theorem: SciLean.ArrayType.one_get
Proof state before:
Cont : Type u_2
Idx : outParam (Type u_3)
Elem : outParam (Type u_1)
inst✝⁴ : IndexType Idx
inst✝³ : outParam (DecidableEq Idx)
inst✝² : LawfulIndexType Idx
inst✝¹ : ArrayType Cont Idx Elem
inst✝ : One Elem
i : Idx
⊢ 1[i] = 1
Tactic:
simp[One.one,OfNat.ofNat]
Proof state after:
no goals
Theorem: SciLean.ArrayType.zero_get
Proof state before:
Cont : Type u_2
Idx : outParam (Type u_3)
Elem : outParam (Type u_1)
inst✝⁴ : IndexType Idx
inst✝³ : outParam (DecidableEq Idx)
inst✝² : LawfulIndexType Idx
inst✝¹ : ArrayType Cont Idx Elem
inst✝ : Zero Elem
i : Idx
⊢ 0[i] = 0
Tactic:
simp[Zero.zero,OfNat.ofNat]
Proof state after:
no goals
Theorem: SciLean.distribDifferentiableAt_const_test_fun
Proof state before:
R : Type u_1
inst✝⁹ : RealScalar R
W : Type ?u.24034
inst✝⁸ : Vec R W
X : Type u_4
inst✝⁷ : Vec R X
inst✝⁶ : MeasureSpace X
Y : Type u_2
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type u_3
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.25667
inst✝¹ : Vec R U
V : Type ?u.25688
inst✝ : Vec R V
f : X → 𝒟'(Y, Z)
x : X
hf : DistribDifferentiableAt f x
φ : 𝒟 Y
⊢ CDifferentiableAt R (fun x => (f x) φ) x
Tactic:
apply hf
Proof state after:
case a
R : Type u_1
inst✝⁹ : RealScalar R
W : Type ?u.24034
inst✝⁸ : Vec R W
X : Type u_4
inst✝⁷ : Vec R X
inst✝⁶ : MeasureSpace X
Y : Type u_2
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type u_3
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.25667
inst✝¹ : Vec R U
V : Type ?u.25688
inst✝ : Vec R V
f : X → 𝒟'(Y, Z)
x : X
hf : DistribDifferentiableAt f x
φ : 𝒟 Y
⊢ CDifferentiableAt R (fun x => φ) x
Theorem: SciLean.distribDifferentiableAt_const_test_fun
Proof state before:
case a
R : Type u_1
inst✝⁹ : RealScalar R
W : Type ?u.24034
inst✝⁸ : Vec R W
X : Type u_4
inst✝⁷ : Vec R X
inst✝⁶ : MeasureSpace X
Y : Type u_2
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type u_3
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.25667
inst✝¹ : Vec R U
V : Type ?u.25688
inst✝ : Vec R V
f : X → 𝒟'(Y, Z)
x : X
hf : DistribDifferentiableAt f x
φ : 𝒟 Y
⊢ CDifferentiableAt R (fun x => φ) x
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.DistribDiffrentiable.const_rule
Proof state before:
R : Type u_1
inst✝⁹ : RealScalar R
W : Type u_4
inst✝⁸ : Vec R W
X : Type u_2
inst✝⁷ : Vec R X
inst✝⁶ : MeasureSpace X
Y : Type u_3
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.38232
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.39021
inst✝¹ : Vec R U
V : Type ?u.39042
inst✝ : Vec R V
T : 𝒟'(X, Y)
⊢ DistribDifferentiable fun x => T
Tactic:
intro _ φ hφ
Proof state after:
R : Type u_1
inst✝⁹ : RealScalar R
W : Type u_4
inst✝⁸ : Vec R W
X : Type u_2
inst✝⁷ : Vec R X
inst✝⁶ : MeasureSpace X
Y : Type u_3
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.38232
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.39021
inst✝¹ : Vec R U
V : Type ?u.39042
inst✝ : Vec R V
T : 𝒟'(X, Y)
x✝ : W
φ : W → 𝒟 X
hφ : CDifferentiableAt R φ x✝
⊢ CDifferentiableAt R (fun x => ((fun x => T) x) (φ x)) x✝
Theorem: SciLean.DistribDiffrentiable.const_rule
Proof state before:
R : Type u_1
inst✝⁹ : RealScalar R
W : Type u_4
inst✝⁸ : Vec R W
X : Type u_2
inst✝⁷ : Vec R X
inst✝⁶ : MeasureSpace X
Y : Type u_3
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.38232
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.39021
inst✝¹ : Vec R U
V : Type ?u.39042
inst✝ : Vec R V
T : 𝒟'(X, Y)
x✝ : W
φ : W → 𝒟 X
hφ : CDifferentiableAt R φ x✝
⊢ CDifferentiableAt R (fun x => ((fun x => T) x) (φ x)) x✝
Tactic:
simp
Proof state after:
R : Type u_1
inst✝⁹ : RealScalar R
W : Type u_4
inst✝⁸ : Vec R W
X : Type u_2
inst✝⁷ : Vec R X
inst✝⁶ : MeasureSpace X
Y : Type u_3
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.38232
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.39021
inst✝¹ : Vec R U
V : Type ?u.39042
inst✝ : Vec R V
T : 𝒟'(X, Y)
x✝ : W
φ : W → 𝒟 X
hφ : CDifferentiableAt R φ x✝
⊢ CDifferentiableAt R (fun x => T (φ x)) x✝
Theorem: SciLean.DistribDiffrentiable.const_rule
Proof state before:
R : Type u_1
inst✝⁹ : RealScalar R
W : Type u_4
inst✝⁸ : Vec R W
X : Type u_2
inst✝⁷ : Vec R X
inst✝⁶ : MeasureSpace X
Y : Type u_3
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.38232
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.39021
inst✝¹ : Vec R U
V : Type ?u.39042
inst✝ : Vec R V
T : 𝒟'(X, Y)
x✝ : W
φ : W → 𝒟 X
hφ : CDifferentiableAt R φ x✝
⊢ CDifferentiableAt R (fun x => T (φ x)) x✝
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.parDistribDeriv.const_rule
Proof state before:
R : Type u_1
inst✝⁹ : RealScalar R
W : Type u_4
inst✝⁸ : Vec R W
X : Type u_2
inst✝⁷ : Vec R X
inst✝⁶ : MeasureSpace X
Y : Type u_3
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.43269
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.44058
inst✝¹ : Vec R U
V : Type ?u.44079
inst✝ : Vec R V
T : 𝒟'(X, Y)
⊢ (parDistribDeriv fun x => T) = fun w dw => 0
Tactic:
funext w dw
Proof state after:
case h.h
R : Type u_1
inst✝⁹ : RealScalar R
W : Type u_4
inst✝⁸ : Vec R W
X : Type u_2
inst✝⁷ : Vec R X
inst✝⁶ : MeasureSpace X
Y : Type u_3
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.43269
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.44058
inst✝¹ : Vec R U
V : Type ?u.44079
inst✝ : Vec R V
T : 𝒟'(X, Y)
w dw : W
⊢ parDistribDeriv (fun x => T) w dw = 0
Theorem: SciLean.parDistribDeriv.const_rule
Proof state before:
case h.h
R : Type u_1
inst✝⁹ : RealScalar R
W : Type u_4
inst✝⁸ : Vec R W
X : Type u_2
inst✝⁷ : Vec R X
inst✝⁶ : MeasureSpace X
Y : Type u_3
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.43269
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.44058
inst✝¹ : Vec R U
V : Type ?u.44079
inst✝ : Vec R V
T : 𝒟'(X, Y)
w dw : W
⊢ parDistribDeriv (fun x => T) w dw = 0
Tactic:
ext φ
Proof state after:
case h.h.a
R : Type u_1
inst✝⁹ : RealScalar R
W : Type u_4
inst✝⁸ : Vec R W
X : Type u_2
inst✝⁷ : Vec R X
inst✝⁶ : MeasureSpace X
Y : Type u_3
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.43269
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.44058
inst✝¹ : Vec R U
V : Type ?u.44079
inst✝ : Vec R V
T : 𝒟'(X, Y)
w dw : W
φ : 𝒟 X
⊢ (parDistribDeriv (fun x => T) w dw) φ = 0 φ
Theorem: SciLean.parDistribDeriv.const_rule
Proof state before:
case h.h.a
R : Type u_1
inst✝⁹ : RealScalar R
W : Type u_4
inst✝⁸ : Vec R W
X : Type u_2
inst✝⁷ : Vec R X
inst✝⁶ : MeasureSpace X
Y : Type u_3
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.43269
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.44058
inst✝¹ : Vec R U
V : Type ?u.44079
inst✝ : Vec R V
T : 𝒟'(X, Y)
w dw : W
φ : 𝒟 X
⊢ (parDistribDeriv (fun x => T) w dw) φ = 0 φ
Tactic:
unfold parDistribDeriv
Proof state after:
case h.h.a
R : Type u_1
inst✝⁹ : RealScalar R
W : Type u_4
inst✝⁸ : Vec R W
X : Type u_2
inst✝⁷ : Vec R X
inst✝⁶ : MeasureSpace X
Y : Type u_3
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.43269
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.44058
inst✝¹ : Vec R U
V : Type ?u.44079
inst✝ : Vec R V
T : 𝒟'(X, Y)
w dw : W
φ : 𝒟 X
⊢ (fun φ ⊸ ∂ (x':=w;dw), ((fun x => T) x') φ) φ = 0 φ
Theorem: SciLean.parDistribDeriv.const_rule
Proof state before:
case h.h.a
R : Type u_1
inst✝⁹ : RealScalar R
W : Type u_4
inst✝⁸ : Vec R W
X : Type u_2
inst✝⁷ : Vec R X
inst✝⁶ : MeasureSpace X
Y : Type u_3
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.43269
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.44058
inst✝¹ : Vec R U
V : Type ?u.44079
inst✝ : Vec R V
T : 𝒟'(X, Y)
w dw : W
φ : 𝒟 X
⊢ (fun φ ⊸ ∂ (x':=w;dw), ((fun x => T) x') φ) φ = 0 φ
Tactic:
fun_trans
Proof state after:
no goals
Theorem: SciLean.dirac.arg_xy.DistribDiffrentiable_rule
Proof state before:
R : Type u_1
inst✝⁹ : RealScalar R
W : Type u_2
inst✝⁸ : Vec R W
X : Type u_3
inst✝⁷ : Vec R X
inst✝⁶ : MeasureSpace X
Y : Type ?u.47090
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.47883
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.48672
inst✝¹ : Vec R U
V : Type ?u.48693
inst✝ : Vec R V
x : W → X
hx : CDifferentiable R x
⊢ DistribDifferentiable fun w => dirac (x w)
Tactic:
intro x
Proof state after:
R : Type u_1
inst✝⁹ : RealScalar R
W : Type u_2
inst✝⁸ : Vec R W
X : Type u_3
inst✝⁷ : Vec R X
inst✝⁶ : MeasureSpace X
Y : Type ?u.47090
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.47883
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.48672
inst✝¹ : Vec R U
V : Type ?u.48693
inst✝ : Vec R V
x✝ : W → X
hx : CDifferentiable R x✝
x : W
⊢ DistribDifferentiableAt (fun w => dirac (x✝ w)) x
Theorem: SciLean.dirac.arg_xy.DistribDiffrentiable_rule
Proof state before:
R : Type u_1
inst✝⁹ : RealScalar R
W : Type u_2
inst✝⁸ : Vec R W
X : Type u_3
inst✝⁷ : Vec R X
inst✝⁶ : MeasureSpace X
Y : Type ?u.47090
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.47883
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.48672
inst✝¹ : Vec R U
V : Type ?u.48693
inst✝ : Vec R V
x✝ : W → X
hx : CDifferentiable R x✝
x : W
⊢ DistribDifferentiableAt (fun w => dirac (x✝ w)) x
Tactic:
unfold DistribDifferentiableAt
Proof state after:
R : Type u_1
inst✝⁹ : RealScalar R
W : Type u_2
inst✝⁸ : Vec R W
X : Type u_3
inst✝⁷ : Vec R X
inst✝⁶ : MeasureSpace X
Y : Type ?u.47090
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.47883
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.48672
inst✝¹ : Vec R U
V : Type ?u.48693
inst✝ : Vec R V
x✝ : W → X
hx : CDifferentiable R x✝
x : W
⊢ ∀ (φ : W → 𝒟 X), CDifferentiableAt R φ x → CDifferentiableAt R (fun x => ((fun w => dirac (x✝ w)) x) (φ x)) x
Theorem: SciLean.dirac.arg_xy.DistribDiffrentiable_rule
Proof state before:
R : Type u_1
inst✝⁹ : RealScalar R
W : Type u_2
inst✝⁸ : Vec R W
X : Type u_3
inst✝⁷ : Vec R X
inst✝⁶ : MeasureSpace X
Y : Type ?u.47090
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.47883
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.48672
inst✝¹ : Vec R U
V : Type ?u.48693
inst✝ : Vec R V
x✝ : W → X
hx : CDifferentiable R x✝
x : W
⊢ ∀ (φ : W → 𝒟 X), CDifferentiableAt R φ x → CDifferentiableAt R (fun x => ((fun w => dirac (x✝ w)) x) (φ x)) x
Tactic:
intro φ hφ
Proof state after:
R : Type u_1
inst✝⁹ : RealScalar R
W : Type u_2
inst✝⁸ : Vec R W
X : Type u_3
inst✝⁷ : Vec R X
inst✝⁶ : MeasureSpace X
Y : Type ?u.47090
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.47883
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.48672
inst✝¹ : Vec R U
V : Type ?u.48693
inst✝ : Vec R V
x✝ : W → X
hx : CDifferentiable R x✝
x : W
φ : W → 𝒟 X
hφ : CDifferentiableAt R φ x
⊢ CDifferentiableAt R (fun x => ((fun w => dirac (x✝ w)) x) (φ x)) x
Theorem: SciLean.dirac.arg_xy.DistribDiffrentiable_rule
Proof state before:
R : Type u_1
inst✝⁹ : RealScalar R
W : Type u_2
inst✝⁸ : Vec R W
X : Type u_3
inst✝⁷ : Vec R X
inst✝⁶ : MeasureSpace X
Y : Type ?u.47090
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.47883
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.48672
inst✝¹ : Vec R U
V : Type ?u.48693
inst✝ : Vec R V
x✝ : W → X
hx : CDifferentiable R x✝
x : W
φ : W → 𝒟 X
hφ : CDifferentiableAt R φ x
⊢ CDifferentiableAt R (fun x => ((fun w => dirac (x✝ w)) x) (φ x)) x
Tactic:
simp [action_dirac, dirac]
Proof state after:
R : Type u_1
inst✝⁹ : RealScalar R
W : Type u_2
inst✝⁸ : Vec R W
X : Type u_3
inst✝⁷ : Vec R X
inst✝⁶ : MeasureSpace X
Y : Type ?u.47090
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.47883
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.48672
inst✝¹ : Vec R U
V : Type ?u.48693
inst✝ : Vec R V
x✝ : W → X
hx : CDifferentiable R x✝
x : W
φ : W → 𝒟 X
hφ : CDifferentiableAt R φ x
⊢ CDifferentiableAt R (fun x => (φ x) (x✝ x)) x
Theorem: SciLean.dirac.arg_xy.DistribDiffrentiable_rule
Proof state before:
R : Type u_1
inst✝⁹ : RealScalar R
W : Type u_2
inst✝⁸ : Vec R W
X : Type u_3
inst✝⁷ : Vec R X
inst✝⁶ : MeasureSpace X
Y : Type ?u.47090
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.47883
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.48672
inst✝¹ : Vec R U
V : Type ?u.48693
inst✝ : Vec R V
x✝ : W → X
hx : CDifferentiable R x✝
x : W
φ : W → 𝒟 X
hφ : CDifferentiableAt R φ x
⊢ CDifferentiableAt R (fun x => (φ x) (x✝ x)) x
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.dirac.arg_x.parDistribDeriv_rule
Proof state before:
R : Type u_1
inst✝⁹ : RealScalar R
W : Type u_2
inst✝⁸ : Vec R W
X : Type u_3
inst✝⁷ : Vec R X
inst✝⁶ : MeasureSpace X
Y : Type ?u.52604
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.53397
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.54186
inst✝¹ : Vec R U
V : Type ?u.54207
inst✝ : Vec R V
x : W → X
hx : CDifferentiable R x
⊢ (parDistribDeriv fun w => dirac (x w)) = fun w dw =>
    let xdx := ∂> x w dw;
    diracDeriv xdx.1 xdx.2
Tactic:
funext w dw
Proof state after:
case h.h
R : Type u_1
inst✝⁹ : RealScalar R
W : Type u_2
inst✝⁸ : Vec R W
X : Type u_3
inst✝⁷ : Vec R X
inst✝⁶ : MeasureSpace X
Y : Type ?u.52604
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.53397
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.54186
inst✝¹ : Vec R U
V : Type ?u.54207
inst✝ : Vec R V
x : W → X
hx : CDifferentiable R x
w dw : W
⊢ parDistribDeriv (fun w => dirac (x w)) w dw =
    let xdx := ∂> x w dw;
    diracDeriv xdx.1 xdx.2
Theorem: SciLean.dirac.arg_x.parDistribDeriv_rule
Proof state before:
case h.h
R : Type u_1
inst✝⁹ : RealScalar R
W : Type u_2
inst✝⁸ : Vec R W
X : Type u_3
inst✝⁷ : Vec R X
inst✝⁶ : MeasureSpace X
Y : Type ?u.52604
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.53397
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.54186
inst✝¹ : Vec R U
V : Type ?u.54207
inst✝ : Vec R V
x : W → X
hx : CDifferentiable R x
w dw : W
⊢ parDistribDeriv (fun w => dirac (x w)) w dw =
    let xdx := ∂> x w dw;
    diracDeriv xdx.1 xdx.2
Tactic:
ext φ
Proof state after:
case h.h.a
R : Type u_1
inst✝⁹ : RealScalar R
W : Type u_2
inst✝⁸ : Vec R W
X : Type u_3
inst✝⁷ : Vec R X
inst✝⁶ : MeasureSpace X
Y : Type ?u.52604
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.53397
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.54186
inst✝¹ : Vec R U
V : Type ?u.54207
inst✝ : Vec R V
x : W → X
hx : CDifferentiable R x
w dw : W
φ : 𝒟 X
⊢ (parDistribDeriv (fun w => dirac (x w)) w dw) φ =
    (let xdx := ∂> x w dw;
      diracDeriv xdx.1 xdx.2)
      φ
Theorem: SciLean.dirac.arg_x.parDistribDeriv_rule
Proof state before:
case h.h.a
R : Type u_1
inst✝⁹ : RealScalar R
W : Type u_2
inst✝⁸ : Vec R W
X : Type u_3
inst✝⁷ : Vec R X
inst✝⁶ : MeasureSpace X
Y : Type ?u.52604
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.53397
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.54186
inst✝¹ : Vec R U
V : Type ?u.54207
inst✝ : Vec R V
x : W → X
hx : CDifferentiable R x
w dw : W
φ : 𝒟 X
⊢ (parDistribDeriv (fun w => dirac (x w)) w dw) φ =
    (let xdx := ∂> x w dw;
      diracDeriv xdx.1 xdx.2)
      φ
Tactic:
unfold parDistribDeriv dirac diracDeriv
Proof state after:
case h.h.a
R : Type u_1
inst✝⁹ : RealScalar R
W : Type u_2
inst✝⁸ : Vec R W
X : Type u_3
inst✝⁷ : Vec R X
inst✝⁶ : MeasureSpace X
Y : Type ?u.52604
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.53397
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.54186
inst✝¹ : Vec R U
V : Type ?u.54207
inst✝ : Vec R V
x : W → X
hx : CDifferentiable R x
w dw : W
φ : 𝒟 X
⊢ (fun φ ⊸ ∂ (x':=w;dw), ((fun w => fun φ ⊸[R] φ (x w)) x') φ) φ =
    (let xdx := ∂> x w dw;
      fun φ ⊸[R] ∂ ⇑φ xdx.1 xdx.2)
      φ
Theorem: SciLean.dirac.arg_x.parDistribDeriv_rule
Proof state before:
case h.h.a
R : Type u_1
inst✝⁹ : RealScalar R
W : Type u_2
inst✝⁸ : Vec R W
X : Type u_3
inst✝⁷ : Vec R X
inst✝⁶ : MeasureSpace X
Y : Type ?u.52604
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.53397
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.54186
inst✝¹ : Vec R U
V : Type ?u.54207
inst✝ : Vec R V
x : W → X
hx : CDifferentiable R x
w dw : W
φ : 𝒟 X
⊢ (fun φ ⊸ ∂ (x':=w;dw), ((fun w => fun φ ⊸[R] φ (x w)) x') φ) φ =
    (let xdx := ∂> x w dw;
      fun φ ⊸[R] ∂ ⇑φ xdx.1 xdx.2)
      φ
Tactic:
simp [pure, fwdDeriv, DistribDifferentiableAt]
Proof state after:
case h.h.a
R : Type u_1
inst✝⁹ : RealScalar R
W : Type u_2
inst✝⁸ : Vec R W
X : Type u_3
inst✝⁷ : Vec R X
inst✝⁶ : MeasureSpace X
Y : Type ?u.52604
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.53397
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.54186
inst✝¹ : Vec R U
V : Type ?u.54207
inst✝ : Vec R V
x : W → X
hx : CDifferentiable R x
w dw : W
φ : 𝒟 X
⊢ ∂ (x':=w;dw), φ (x x') = ∂ ⇑φ (x w) (∂ x w dw)
Theorem: SciLean.dirac.arg_x.parDistribDeriv_rule
Proof state before:
case h.h.a
R : Type u_1
inst✝⁹ : RealScalar R
W : Type u_2
inst✝⁸ : Vec R W
X : Type u_3
inst✝⁷ : Vec R X
inst✝⁶ : MeasureSpace X
Y : Type ?u.52604
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.53397
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.54186
inst✝¹ : Vec R U
V : Type ?u.54207
inst✝ : Vec R V
x : W → X
hx : CDifferentiable R x
w dw : W
φ : 𝒟 X
⊢ ∂ (x':=w;dw), φ (x x') = ∂ ⇑φ (x w) (∂ x w dw)
Tactic:
fun_trans
Proof state after:
no goals
Theorem: SciLean.DistribDiffrentiable.comp_rule
Proof state before:
R : Type u_1
inst✝⁹ : RealScalar R
W : Type ?u.64347
inst✝⁸ : Vec R W
X : Type u_5
inst✝⁷ : Vec R X
inst✝⁶ : MeasureSpace X
Y : Type u_4
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type u_2
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type u_3
inst✝¹ : Vec R U
V : Type ?u.66001
inst✝ : Vec R V
f : Y → 𝒟'(Z, U)
g : X → Y
hf : DistribDifferentiable f
hg : CDifferentiable R g
⊢ DistribDifferentiable fun x => f (g x)
Tactic:
intro x
Proof state after:
R : Type u_1
inst✝⁹ : RealScalar R
W : Type ?u.64347
inst✝⁸ : Vec R W
X : Type u_5
inst✝⁷ : Vec R X
inst✝⁶ : MeasureSpace X
Y : Type u_4
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type u_2
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type u_3
inst✝¹ : Vec R U
V : Type ?u.66001
inst✝ : Vec R V
f : Y → 𝒟'(Z, U)
g : X → Y
hf : DistribDifferentiable f
hg : CDifferentiable R g
x : X
⊢ DistribDifferentiableAt (fun x => f (g x)) x
Theorem: SciLean.DistribDiffrentiable.comp_rule
Proof state before:
R : Type u_1
inst✝⁹ : RealScalar R
W : Type ?u.64347
inst✝⁸ : Vec R W
X : Type u_5
inst✝⁷ : Vec R X
inst✝⁶ : MeasureSpace X
Y : Type u_4
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type u_2
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type u_3
inst✝¹ : Vec R U
V : Type ?u.66001
inst✝ : Vec R V
f : Y → 𝒟'(Z, U)
g : X → Y
hf : DistribDifferentiable f
hg : CDifferentiable R g
x : X
⊢ DistribDifferentiableAt (fun x => f (g x)) x
Tactic:
unfold DistribDifferentiableAt
Proof state after:
R : Type u_1
inst✝⁹ : RealScalar R
W : Type ?u.64347
inst✝⁸ : Vec R W
X : Type u_5
inst✝⁷ : Vec R X
inst✝⁶ : MeasureSpace X
Y : Type u_4
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type u_2
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type u_3
inst✝¹ : Vec R U
V : Type ?u.66001
inst✝ : Vec R V
f : Y → 𝒟'(Z, U)
g : X → Y
hf : DistribDifferentiable f
hg : CDifferentiable R g
x : X
⊢ ∀ (φ : X → 𝒟 Z), CDifferentiableAt R φ x → CDifferentiableAt R (fun x => ((fun x => f (g x)) x) (φ x)) x
Theorem: SciLean.DistribDiffrentiable.comp_rule
Proof state before:
R : Type u_1
inst✝⁹ : RealScalar R
W : Type ?u.64347
inst✝⁸ : Vec R W
X : Type u_5
inst✝⁷ : Vec R X
inst✝⁶ : MeasureSpace X
Y : Type u_4
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type u_2
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type u_3
inst✝¹ : Vec R U
V : Type ?u.66001
inst✝ : Vec R V
f : Y → 𝒟'(Z, U)
g : X → Y
hf : DistribDifferentiable f
hg : CDifferentiable R g
x : X
⊢ ∀ (φ : X → 𝒟 Z), CDifferentiableAt R φ x → CDifferentiableAt R (fun x => ((fun x => f (g x)) x) (φ x)) x
Tactic:
intro φ hφ
Proof state after:
R : Type u_1
inst✝⁹ : RealScalar R
W : Type ?u.64347
inst✝⁸ : Vec R W
X : Type u_5
inst✝⁷ : Vec R X
inst✝⁶ : MeasureSpace X
Y : Type u_4
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type u_2
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type u_3
inst✝¹ : Vec R U
V : Type ?u.66001
inst✝ : Vec R V
f : Y → 𝒟'(Z, U)
g : X → Y
hf : DistribDifferentiable f
hg : CDifferentiable R g
x : X
φ : X → 𝒟 Z
hφ : CDifferentiableAt R φ x
⊢ CDifferentiableAt R (fun x => ((fun x => f (g x)) x) (φ x)) x
Theorem: SciLean.DistribDiffrentiable.comp_rule
Proof state before:
R : Type u_1
inst✝⁹ : RealScalar R
W : Type ?u.64347
inst✝⁸ : Vec R W
X : Type u_5
inst✝⁷ : Vec R X
inst✝⁶ : MeasureSpace X
Y : Type u_4
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type u_2
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type u_3
inst✝¹ : Vec R U
V : Type ?u.66001
inst✝ : Vec R V
f : Y → 𝒟'(Z, U)
g : X → Y
hf : DistribDifferentiable f
hg : CDifferentiable R g
x : X
φ : X → 𝒟 Z
hφ : CDifferentiableAt R φ x
⊢ CDifferentiableAt R (fun x => ((fun x => f (g x)) x) (φ x)) x
Tactic:
apply CDifferentiable.comp_rule (K:=R) (f:=fun xy : X×Y => f xy.2 (φ xy.1)) (g:=fun x => (x, g x))
  (hg:=by fun_prop)
Proof state after:
case hf
R : Type u_1
inst✝⁹ : RealScalar R
W : Type ?u.64347
inst✝⁸ : Vec R W
X : Type u_5
inst✝⁷ : Vec R X
inst✝⁶ : MeasureSpace X
Y : Type u_4
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type u_2
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type u_3
inst✝¹ : Vec R U
V : Type ?u.66001
inst✝ : Vec R V
f : Y → 𝒟'(Z, U)
g : X → Y
hf : DistribDifferentiable f
hg : CDifferentiable R g
x : X
φ : X → 𝒟 Z
hφ : CDifferentiableAt R φ x
⊢ CDifferentiable R fun xy => (f xy.2) (φ xy.1)