internlm/Lean-Github huggingface dataset:
Theorem: SciLean.Prod.mk.arg_fstsnd.CDifferentiable_rule
Proof state before:
K✝ : Type ?u.6642
inst✝¹¹ : RCLike K✝
X✝ : Type ?u.6648
inst✝¹⁰ : Vec K✝ X✝
Y✝ : Type ?u.6661
inst✝⁹ : Vec K✝ Y✝
Z✝ : Type ?u.6672
inst✝⁸ : Vec K✝ Z✝
ι✝ : Type ?u.6683
inst✝⁷ : IndexType ι✝
E✝ : ι✝ → Type ?u.6692
inst✝⁶ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_1
inst✝⁵ : RCLike K
X : Type u_2
inst✝⁴ : Vec K X
Y : Type u_3
inst✝³ : Vec K Y
Z : Type u_4
inst✝² : Vec K Z
ι : Type ?u.6749
inst✝¹ : IndexType ι
E : ι → Type ?u.6758
inst✝ : (i : ι) → Vec K (E i)
g : X → Y
hg : CDifferentiable K g
f : X → Z
hf : CDifferentiable K f
x : X
⊢ CDifferentiableAt K (fun x => (g x, f x)) x
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.Prod.fst.arg_self.CDifferentiable_rule
Proof state before:
K✝ : Type ?u.7215
inst✝¹¹ : RCLike K✝
X✝ : Type ?u.7221
inst✝¹⁰ : Vec K✝ X✝
Y✝ : Type ?u.7234
inst✝⁹ : Vec K✝ Y✝
Z✝ : Type ?u.7245
inst✝⁸ : Vec K✝ Z✝
ι✝ : Type ?u.7256
inst✝⁷ : IndexType ι✝
E✝ : ι✝ → Type ?u.7265
inst✝⁶ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_3
inst✝⁵ : RCLike K
X : Type u_4
inst✝⁴ : Vec K X
Y : Type u_1
inst✝³ : Vec K Y
Z : Type u_2
inst✝² : Vec K Z
ι : Type ?u.7322
inst✝¹ : IndexType ι
E : ι → Type ?u.7331
inst✝ : (i : ι) → Vec K (E i)
f : X → Y × Z
hf : CDifferentiable K f
⊢ CDifferentiable K fun x => (f x).1
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Prod.fst.arg_self.CDifferentiableAt_rule
Proof state before:
K✝ : Type ?u.7502
inst✝¹¹ : RCLike K✝
X✝ : Type ?u.7508
inst✝¹⁰ : Vec K✝ X✝
Y✝ : Type ?u.7521
inst✝⁹ : Vec K✝ Y✝
Z✝ : Type ?u.7532
inst✝⁸ : Vec K✝ Z✝
ι✝ : Type ?u.7543
inst✝⁷ : IndexType ι✝
E✝ : ι✝ → Type ?u.7552
inst✝⁶ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_3
inst✝⁵ : RCLike K
X : Type u_4
inst✝⁴ : Vec K X
Y : Type u_1
inst✝³ : Vec K Y
Z : Type u_2
inst✝² : Vec K Z
ι : Type ?u.7609
inst✝¹ : IndexType ι
E : ι → Type ?u.7618
inst✝ : (i : ι) → Vec K (E i)
x : X
f : X → Y × Z
hf : CDifferentiableAt K f x
⊢ CDifferentiableAt K (fun x => (f x).1) x
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.Prod.snd.arg_self.CDifferentiable_rule
Proof state before:
K✝ : Type ?u.8049
inst✝¹¹ : RCLike K✝
X✝ : Type ?u.8055
inst✝¹⁰ : Vec K✝ X✝
Y✝ : Type ?u.8068
inst✝⁹ : Vec K✝ Y✝
Z✝ : Type ?u.8079
inst✝⁸ : Vec K✝ Z✝
ι✝ : Type ?u.8090
inst✝⁷ : IndexType ι✝
E✝ : ι✝ → Type ?u.8099
inst✝⁶ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_3
inst✝⁵ : RCLike K
X : Type u_4
inst✝⁴ : Vec K X
Y : Type u_1
inst✝³ : Vec K Y
Z : Type u_2
inst✝² : Vec K Z
ι : Type ?u.8156
inst✝¹ : IndexType ι
E : ι → Type ?u.8165
inst✝ : (i : ι) → Vec K (E i)
f : X → Y × Z
hf : CDifferentiable K f
⊢ CDifferentiable K fun x => (f x).2
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Prod.snd.arg_self.CDifferentiableAt_rule
Proof state before:
K✝ : Type ?u.8336
inst✝¹¹ : RCLike K✝
X✝ : Type ?u.8342
inst✝¹⁰ : Vec K✝ X✝
Y✝ : Type ?u.8355
inst✝⁹ : Vec K✝ Y✝
Z✝ : Type ?u.8366
inst✝⁸ : Vec K✝ Z✝
ι✝ : Type ?u.8377
inst✝⁷ : IndexType ι✝
E✝ : ι✝ → Type ?u.8386
inst✝⁶ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_3
inst✝⁵ : RCLike K
X : Type u_4
inst✝⁴ : Vec K X
Y : Type u_1
inst✝³ : Vec K Y
Z : Type u_2
inst✝² : Vec K Z
ι : Type ?u.8443
inst✝¹ : IndexType ι
E : ι → Type ?u.8452
inst✝ : (i : ι) → Vec K (E i)
x : X
f : X → Y × Z
hf : CDifferentiableAt K f x
⊢ CDifferentiableAt K (fun x => (f x).2) x
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.Neg.neg.arg_a0.CDifferentiable_rule
Proof state before:
K✝ : Type ?u.8883
inst✝¹¹ : RCLike K✝
X✝ : Type ?u.8889
inst✝¹⁰ : Vec K✝ X✝
Y✝ : Type ?u.8902
inst✝⁹ : Vec K✝ Y✝
Z✝ : Type ?u.8913
inst✝⁸ : Vec K✝ Z✝
ι✝ : Type ?u.8924
inst✝⁷ : IndexType ι✝
E✝ : ι✝ → Type ?u.8933
inst✝⁶ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_1
inst✝⁵ : RCLike K
X : Type u_2
inst✝⁴ : Vec K X
Y : Type u_3
inst✝³ : Vec K Y
Z : Type ?u.8979
inst✝² : Vec K Z
ι : Type ?u.8990
inst✝¹ : IndexType ι
E : ι → Type ?u.8999
inst✝ : (i : ι) → Vec K (E i)
f : X → Y
hf : CDifferentiable K f
⊢ CDifferentiable K fun x => -f x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Neg.neg.arg_a0.CDifferentiableAt_rule
Proof state before:
K✝ : Type ?u.9364
inst✝¹¹ : RCLike K✝
X✝ : Type ?u.9370
inst✝¹⁰ : Vec K✝ X✝
Y✝ : Type ?u.9383
inst✝⁹ : Vec K✝ Y✝
Z✝ : Type ?u.9394
inst✝⁸ : Vec K✝ Z✝
ι✝ : Type ?u.9405
inst✝⁷ : IndexType ι✝
E✝ : ι✝ → Type ?u.9414
inst✝⁶ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_1
inst✝⁵ : RCLike K
X : Type u_2
inst✝⁴ : Vec K X
Y : Type u_3
inst✝³ : Vec K Y
Z : Type ?u.9460
inst✝² : Vec K Z
ι : Type ?u.9471
inst✝¹ : IndexType ι
E : ι → Type ?u.9480
inst✝ : (i : ι) → Vec K (E i)
x : X
f : X → Y
hf : CDifferentiableAt K f x
⊢ CDifferentiableAt K (fun x => -f x) x
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.HAdd.hAdd.arg_a0a1.CDifferentiable_rule
Proof state before:
K✝ : Type ?u.10041
inst✝¹¹ : RCLike K✝
X✝ : Type ?u.10047
inst✝¹⁰ : Vec K✝ X✝
Y✝ : Type ?u.10060
inst✝⁹ : Vec K✝ Y✝
Z✝ : Type ?u.10071
inst✝⁸ : Vec K✝ Z✝
ι✝ : Type ?u.10082
inst✝⁷ : IndexType ι✝
E✝ : ι✝ → Type ?u.10091
inst✝⁶ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_1
inst✝⁵ : RCLike K
X : Type u_2
inst✝⁴ : Vec K X
Y : Type u_3
inst✝³ : Vec K Y
Z : Type ?u.10137
inst✝² : Vec K Z
ι : Type ?u.10148
inst✝¹ : IndexType ι
E : ι → Type ?u.10157
inst✝ : (i : ι) → Vec K (E i)
f g : X → Y
hf : CDifferentiable K f
hg : CDifferentiable K g
⊢ CDifferentiable K fun x => f x + g x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.HAdd.hAdd.arg_a0a1.CDifferentiableAt_rule
Proof state before:
K✝ : Type ?u.11441
inst✝¹¹ : RCLike K✝
X✝ : Type ?u.11447
inst✝¹⁰ : Vec K✝ X✝
Y✝ : Type ?u.11460
inst✝⁹ : Vec K✝ Y✝
Z✝ : Type ?u.11471
inst✝⁸ : Vec K✝ Z✝
ι✝ : Type ?u.11482
inst✝⁷ : IndexType ι✝
E✝ : ι✝ → Type ?u.11491
inst✝⁶ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_1
inst✝⁵ : RCLike K
X : Type u_2
inst✝⁴ : Vec K X
Y : Type u_3
inst✝³ : Vec K Y
Z : Type ?u.11537
inst✝² : Vec K Z
ι : Type ?u.11548
inst✝¹ : IndexType ι
E : ι → Type ?u.11557
inst✝ : (i : ι) → Vec K (E i)
x : X
f g : X → Y
hf : CDifferentiableAt K f x
hg : CDifferentiableAt K g x
⊢ CDifferentiableAt K (fun x => f x + g x) x
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.HSub.hSub.arg_a0a1.CDifferentiable_rule
Proof state before:
K✝ : Type ?u.13259
inst✝¹¹ : RCLike K✝
X✝ : Type ?u.13265
inst✝¹⁰ : Vec K✝ X✝
Y✝ : Type ?u.13278
inst✝⁹ : Vec K✝ Y✝
Z✝ : Type ?u.13289
inst✝⁸ : Vec K✝ Z✝
ι✝ : Type ?u.13300
inst✝⁷ : IndexType ι✝
E✝ : ι✝ → Type ?u.13309
inst✝⁶ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_1
inst✝⁵ : RCLike K
X : Type u_2
inst✝⁴ : Vec K X
Y : Type u_3
inst✝³ : Vec K Y
Z : Type ?u.13355
inst✝² : Vec K Z
ι : Type ?u.13366
inst✝¹ : IndexType ι
E : ι → Type ?u.13375
inst✝ : (i : ι) → Vec K (E i)
f g : X → Y
hf : CDifferentiable K f
hg : CDifferentiable K g
⊢ CDifferentiable K fun x => f x - g x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.HSub.hSub.arg_a0a1.CDifferentiableAt_rule
Proof state before:
K✝ : Type ?u.14123
inst✝¹¹ : RCLike K✝
X✝ : Type ?u.14129
inst✝¹⁰ : Vec K✝ X✝
Y✝ : Type ?u.14142
inst✝⁹ : Vec K✝ Y✝
Z✝ : Type ?u.14153
inst✝⁸ : Vec K✝ Z✝
ι✝ : Type ?u.14164
inst✝⁷ : IndexType ι✝
E✝ : ι✝ → Type ?u.14173
inst✝⁶ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_1
inst✝⁵ : RCLike K
X : Type u_2
inst✝⁴ : Vec K X
Y : Type u_3
inst✝³ : Vec K Y
Z : Type ?u.14219
inst✝² : Vec K Z
ι : Type ?u.14230
inst✝¹ : IndexType ι
E : ι → Type ?u.14239
inst✝ : (i : ι) → Vec K (E i)
x : X
f g : X → Y
hf : CDifferentiableAt K f x
hg : CDifferentiableAt K g x
⊢ CDifferentiableAt K (fun x => f x - g x) x
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.HSMul.hSMul.arg_a1.CDifferentiable_rule_nat
Proof state before:
K✝ : Type ?u.20769
inst✝¹¹ : RCLike K✝
X✝ : Type ?u.20775
inst✝¹⁰ : Vec K✝ X✝
Y✝ : Type ?u.20788
inst✝⁹ : Vec K✝ Y✝
Z✝ : Type ?u.20799
inst✝⁸ : Vec K✝ Z✝
ι✝ : Type ?u.20810
inst✝⁷ : IndexType ι✝
E✝ : ι✝ → Type ?u.20819
inst✝⁶ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_1
inst✝⁵ : RCLike K
X : Type u_2
inst✝⁴ : Vec K X
Y : Type u_3
inst✝³ : Vec K Y
Z : Type ?u.20865
inst✝² : Vec K Z
ι : Type ?u.20876
inst✝¹ : IndexType ι
E : ι → Type ?u.20885
inst✝ : (i : ι) → Vec K (E i)
c : ℕ
f : X → Y
hf : CDifferentiable K f
⊢ CDifferentiable K fun x => c • f x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.HSMul.hSMul.arg_a1.CDifferentiableAt_rule_nat
Proof state before:
K✝ : Type ?u.21513
inst✝¹¹ : RCLike K✝
X✝ : Type ?u.21519
inst✝¹⁰ : Vec K✝ X✝
Y✝ : Type ?u.21532
inst✝⁹ : Vec K✝ Y✝
Z✝ : Type ?u.21543
inst✝⁸ : Vec K✝ Z✝
ι✝ : Type ?u.21554
inst✝⁷ : IndexType ι✝
E✝ : ι✝ → Type ?u.21563
inst✝⁶ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_1
inst✝⁵ : RCLike K
X : Type u_2
inst✝⁴ : Vec K X
Y : Type u_3
inst✝³ : Vec K Y
Z : Type ?u.21609
inst✝² : Vec K Z
ι : Type ?u.21620
inst✝¹ : IndexType ι
E : ι → Type ?u.21629
inst✝ : (i : ι) → Vec K (E i)
c : ℕ
f : X → Y
x : X
hf : CDifferentiableAt K f x
⊢ CDifferentiableAt K (fun x => c • f x) x
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.HSMul.hSMul.arg_a1.CDifferentiable_rule_int
Proof state before:
K✝ : Type ?u.22523
inst✝¹¹ : RCLike K✝
X✝ : Type ?u.22529
inst✝¹⁰ : Vec K✝ X✝
Y✝ : Type ?u.22542
inst✝⁹ : Vec K✝ Y✝
Z✝ : Type ?u.22553
inst✝⁸ : Vec K✝ Z✝
ι✝ : Type ?u.22564
inst✝⁷ : IndexType ι✝
E✝ : ι✝ → Type ?u.22573
inst✝⁶ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_1
inst✝⁵ : RCLike K
X : Type u_2
inst✝⁴ : Vec K X
Y : Type u_3
inst✝³ : Vec K Y
Z : Type ?u.22619
inst✝² : Vec K Z
ι : Type ?u.22630
inst✝¹ : IndexType ι
E : ι → Type ?u.22639
inst✝ : (i : ι) → Vec K (E i)
c : ℤ
f : X → Y
hf : CDifferentiable K f
⊢ CDifferentiable K fun x => c • f x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.HSMul.hSMul.arg_a1.CDifferentiableAt_rule_int
Proof state before:
K✝ : Type ?u.23095
inst✝¹¹ : RCLike K✝
X✝ : Type ?u.23101
inst✝¹⁰ : Vec K✝ X✝
Y✝ : Type ?u.23114
inst✝⁹ : Vec K✝ Y✝
Z✝ : Type ?u.23125
inst✝⁸ : Vec K✝ Z✝
ι✝ : Type ?u.23136
inst✝⁷ : IndexType ι✝
E✝ : ι✝ → Type ?u.23145
inst✝⁶ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_1
inst✝⁵ : RCLike K
X : Type u_2
inst✝⁴ : Vec K X
Y : Type u_3
inst✝³ : Vec K Y
Z : Type ?u.23191
inst✝² : Vec K Z
ι : Type ?u.23202
inst✝¹ : IndexType ι
E : ι → Type ?u.23211
inst✝ : (i : ι) → Vec K (E i)
c : ℤ
f : X → Y
x : X
hf : CDifferentiableAt K f x
⊢ CDifferentiableAt K (fun x => c • f x) x
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.IndexType.sum.arg_f.CDifferentiableAt_rule
Proof state before:
K✝ : Type ?u.28348
inst✝¹¹ : RCLike K✝
X✝ : Type ?u.28354
inst✝¹⁰ : Vec K✝ X✝
Y✝ : Type ?u.28367
inst✝⁹ : Vec K✝ Y✝
Z✝ : Type ?u.28378
inst✝⁸ : Vec K✝ Z✝
ι✝ : Type ?u.28389
inst✝⁷ : IndexType ι✝
E✝ : ι✝ → Type ?u.28398
inst✝⁶ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_1
inst✝⁵ : RCLike K
X : Type u_2
inst✝⁴ : Vec K X
Y : Type u_3
inst✝³ : Vec K Y
Z : Type ?u.28444
inst✝² : Vec K Z
ι : Type u_4
inst✝¹ : IndexType ι
E : ι → Type ?u.28464
inst✝ : (i : ι) → Vec K (E i)
f : X → ι → Y
x : X
hf : ∀ (i : ι), CDifferentiableAt K (fun x => f x i) x
⊢ CDifferentiableAt K (fun x =>  ∑ i, f x i) x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.IndexType.sum.arg_f.CDifferentiable_rule
Proof state before:
K✝ : Type ?u.30023
inst✝¹¹ : RCLike K✝
X✝ : Type ?u.30029
inst✝¹⁰ : Vec K✝ X✝
Y✝ : Type ?u.30042
inst✝⁹ : Vec K✝ Y✝
Z✝ : Type ?u.30053
inst✝⁸ : Vec K✝ Z✝
ι✝ : Type ?u.30064
inst✝⁷ : IndexType ι✝
E✝ : ι✝ → Type ?u.30073
inst✝⁶ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_1
inst✝⁵ : RCLike K
X : Type u_2
inst✝⁴ : Vec K X
Y : Type u_3
inst✝³ : Vec K Y
Z : Type ?u.30119
inst✝² : Vec K Z
ι : Type u_4
inst✝¹ : IndexType ι
E : ι → Type ?u.30139
inst✝ : (i : ι) → Vec K (E i)
f : X → ι → Y
hf : ∀ (i : ι), CDifferentiable K fun x => f x i
⊢ CDifferentiable K fun x =>  ∑ i, f x i
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Inner.inner.arg_a0a1.CDifferentiable_rule
Proof state before:
K✝ : Type ?u.31879
inst✝¹⁴ : RCLike K✝
X✝¹ : Type ?u.31885
inst✝¹³ : Vec K✝ X✝¹
Y✝¹ : Type ?u.31898
inst✝¹² : Vec K✝ Y✝¹
Z✝ : Type ?u.31909
inst✝¹¹ : Vec K✝ Z✝
ι✝ : Type ?u.31920
inst✝¹⁰ : IndexType ι✝
E✝ : ι✝ → Type ?u.31929
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.31945
inst✝⁸ : RCLike K
X✝ : Type ?u.31951
inst✝⁷ : Vec K X✝
Y✝ : Type ?u.31964
inst✝⁶ : Vec K Y✝
Z : Type ?u.31975
inst✝⁵ : Vec K Z
ι : Type ?u.31986
inst✝⁴ : IndexType ι
E : ι → Type ?u.31995
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f g : X → Y
hf : CDifferentiable R f
hg : CDifferentiable R g
⊢ CDifferentiable R fun x => ⟪f x, g x⟫_R
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Inner.inner.arg_a0a1.CDifferentiableAt_rule
Proof state before:
K✝ : Type ?u.32359
inst✝¹⁴ : RCLike K✝
X✝¹ : Type ?u.32365
inst✝¹³ : Vec K✝ X✝¹
Y✝¹ : Type ?u.32378
inst✝¹² : Vec K✝ Y✝¹
Z✝ : Type ?u.32389
inst✝¹¹ : Vec K✝ Z✝
ι✝ : Type ?u.32400
inst✝¹⁰ : IndexType ι✝
E✝ : ι✝ → Type ?u.32409
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.32425
inst✝⁸ : RCLike K
X✝ : Type ?u.32431
inst✝⁷ : Vec K X✝
Y✝ : Type ?u.32444
inst✝⁶ : Vec K Y✝
Z : Type ?u.32455
inst✝⁵ : Vec K Z
ι : Type ?u.32466
inst✝⁴ : IndexType ι
E : ι → Type ?u.32475
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f g : X → Y
x : X
hf : CDifferentiableAt R f x
hg : CDifferentiableAt R g x
⊢ CDifferentiableAt R (fun x => ⟪f x, g x⟫_R) x
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.SciLean.Norm2.norm2.arg_a0.CDifferentiable_rule
Proof state before:
K✝ : Type ?u.33370
inst✝¹⁴ : RCLike K✝
X✝¹ : Type ?u.33376
inst✝¹³ : Vec K✝ X✝¹
Y✝¹ : Type ?u.33389
inst✝¹² : Vec K✝ Y✝¹
Z✝ : Type ?u.33400
inst✝¹¹ : Vec K✝ Z✝
ι✝ : Type ?u.33411
inst✝¹⁰ : IndexType ι✝
E✝ : ι✝ → Type ?u.33420
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.33436
inst✝⁸ : RCLike K
X✝ : Type ?u.33442
inst✝⁷ : Vec K X✝
Y✝ : Type ?u.33455
inst✝⁶ : Vec K Y✝
Z : Type ?u.33466
inst✝⁵ : Vec K Z
ι : Type ?u.33477
inst✝⁴ : IndexType ι
E : ι → Type ?u.33486
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
hf : CDifferentiable R f
⊢ CDifferentiable R fun x => ‖f x‖₂²
Tactic:
simp[← SemiInnerProductSpace.inner_norm2]
Proof state after:
K✝ : Type ?u.33370
inst✝¹⁴ : RCLike K✝
X✝¹ : Type ?u.33376
inst✝¹³ : Vec K✝ X✝¹
Y✝¹ : Type ?u.33389
inst✝¹² : Vec K✝ Y✝¹
Z✝ : Type ?u.33400
inst✝¹¹ : Vec K✝ Z✝
ι✝ : Type ?u.33411
inst✝¹⁰ : IndexType ι✝
E✝ : ι✝ → Type ?u.33420
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.33436
inst✝⁸ : RCLike K
X✝ : Type ?u.33442
inst✝⁷ : Vec K X✝
Y✝ : Type ?u.33455
inst✝⁶ : Vec K Y✝
Z : Type ?u.33466
inst✝⁵ : Vec K Z
ι : Type ?u.33477
inst✝⁴ : IndexType ι
E : ι → Type ?u.33486
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
hf : CDifferentiable R f
⊢ CDifferentiable R fun x => ⟪f x, f x⟫_R
Theorem: SciLean.SciLean.Norm2.norm2.arg_a0.CDifferentiable_rule
Proof state before:
K✝ : Type ?u.33370
inst✝¹⁴ : RCLike K✝
X✝¹ : Type ?u.33376
inst✝¹³ : Vec K✝ X✝¹
Y✝¹ : Type ?u.33389
inst✝¹² : Vec K✝ Y✝¹
Z✝ : Type ?u.33400
inst✝¹¹ : Vec K✝ Z✝
ι✝ : Type ?u.33411
inst✝¹⁰ : IndexType ι✝
E✝ : ι✝ → Type ?u.33420
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.33436
inst✝⁸ : RCLike K
X✝ : Type ?u.33442
inst✝⁷ : Vec K X✝
Y✝ : Type ?u.33455
inst✝⁶ : Vec K Y✝
Z : Type ?u.33466
inst✝⁵ : Vec K Z
ι : Type ?u.33477
inst✝⁴ : IndexType ι
E : ι → Type ?u.33486
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
hf : CDifferentiable R f
⊢ CDifferentiable R fun x => ⟪f x, f x⟫_R
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.SciLean.Norm2.norm2.arg_a0.CDifferentiableAt_rule
Proof state before:
K✝ : Type ?u.34717
inst✝¹⁴ : RCLike K✝
X✝¹ : Type ?u.34723
inst✝¹³ : Vec K✝ X✝¹
Y✝¹ : Type ?u.34736
inst✝¹² : Vec K✝ Y✝¹
Z✝ : Type ?u.34747
inst✝¹¹ : Vec K✝ Z✝
ι✝ : Type ?u.34758
inst✝¹⁰ : IndexType ι✝
E✝ : ι✝ → Type ?u.34767
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.34783
inst✝⁸ : RCLike K
X✝ : Type ?u.34789
inst✝⁷ : Vec K X✝
Y✝ : Type ?u.34802
inst✝⁶ : Vec K Y✝
Z : Type ?u.34813
inst✝⁵ : Vec K Z
ι : Type ?u.34824
inst✝⁴ : IndexType ι
E : ι → Type ?u.34833
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
x : X
hf : CDifferentiableAt R f x
⊢ CDifferentiableAt R (fun x => ‖f x‖₂²) x
Tactic:
simp[← SemiInnerProductSpace.inner_norm2]
Proof state after:
K✝ : Type ?u.34717
inst✝¹⁴ : RCLike K✝
X✝¹ : Type ?u.34723
inst✝¹³ : Vec K✝ X✝¹
Y✝¹ : Type ?u.34736
inst✝¹² : Vec K✝ Y✝¹
Z✝ : Type ?u.34747
inst✝¹¹ : Vec K✝ Z✝
ι✝ : Type ?u.34758
inst✝¹⁰ : IndexType ι✝
E✝ : ι✝ → Type ?u.34767
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.34783
inst✝⁸ : RCLike K
X✝ : Type ?u.34789
inst✝⁷ : Vec K X✝
Y✝ : Type ?u.34802
inst✝⁶ : Vec K Y✝
Z : Type ?u.34813
inst✝⁵ : Vec K Z
ι : Type ?u.34824
inst✝⁴ : IndexType ι
E : ι → Type ?u.34833
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
x : X
hf : CDifferentiableAt R f x
⊢ CDifferentiableAt R (fun x => ⟪f x, f x⟫_R) x
Theorem: SciLean.SciLean.Norm2.norm2.arg_a0.CDifferentiableAt_rule
Proof state before:
K✝ : Type ?u.34717
inst✝¹⁴ : RCLike K✝
X✝¹ : Type ?u.34723
inst✝¹³ : Vec K✝ X✝¹
Y✝¹ : Type ?u.34736
inst✝¹² : Vec K✝ Y✝¹
Z✝ : Type ?u.34747
inst✝¹¹ : Vec K✝ Z✝
ι✝ : Type ?u.34758
inst✝¹⁰ : IndexType ι✝
E✝ : ι✝ → Type ?u.34767
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.34783
inst✝⁸ : RCLike K
X✝ : Type ?u.34789
inst✝⁷ : Vec K X✝
Y✝ : Type ?u.34802
inst✝⁶ : Vec K Y✝
Z : Type ?u.34813
inst✝⁵ : Vec K Z
ι : Type ?u.34824
inst✝⁴ : IndexType ι
E : ι → Type ?u.34833
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
x : X
hf : CDifferentiableAt R f x
⊢ CDifferentiableAt R (fun x => ⟪f x, f x⟫_R) x
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.SciLean.norm₂.arg_x.CDifferentiable_rule
Proof state before:
K✝ : Type ?u.36079
inst✝¹⁴ : RCLike K✝
X✝¹ : Type ?u.36085
inst✝¹³ : Vec K✝ X✝¹
Y✝¹ : Type ?u.36098
inst✝¹² : Vec K✝ Y✝¹
Z✝ : Type ?u.36109
inst✝¹¹ : Vec K✝ Z✝
ι✝ : Type ?u.36120
inst✝¹⁰ : IndexType ι✝
E✝ : ι✝ → Type ?u.36129
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.36145
inst✝⁸ : RCLike K
X✝ : Type ?u.36151
inst✝⁷ : Vec K X✝
Y✝ : Type ?u.36164
inst✝⁶ : Vec K Y✝
Z : Type ?u.36175
inst✝⁵ : Vec K Z
ι : Type ?u.36186
inst✝⁴ : IndexType ι
E : ι → Type ?u.36195
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
x : X
f : X → Y
hf : CDifferentiable R f
hx : f x ≠ 0
⊢ CDifferentiable R fun x => ‖f x‖₂[R]
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.SciLean.norm₂.arg_x.CDifferentiableAt_rule
Proof state before:
K✝ : Type ?u.37534
inst✝¹⁴ : RCLike K✝
X✝¹ : Type ?u.37540
inst✝¹³ : Vec K✝ X✝¹
Y✝¹ : Type ?u.37553
inst✝¹² : Vec K✝ Y✝¹
Z✝ : Type ?u.37564
inst✝¹¹ : Vec K✝ Z✝
ι✝ : Type ?u.37575
inst✝¹⁰ : IndexType ι✝
E✝ : ι✝ → Type ?u.37584
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.37600
inst✝⁸ : RCLike K
X✝ : Type ?u.37606
inst✝⁷ : Vec K X✝
Y✝ : Type ?u.37619
inst✝⁶ : Vec K Y✝
Z : Type ?u.37630
inst✝⁵ : Vec K Z
ι : Type ?u.37641
inst✝⁴ : IndexType ι
E : ι → Type ?u.37650
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
x : X
hf : CDifferentiableAt R f x
hx : f x ≠ 0
⊢ CDifferentiableAt R (fun x => ‖f x‖₂[R]) x
Tactic:
fun_prop (disch:=assumption)
Proof state after:
no goals
Theorem: SciLean.SciLean.norm₂.arg_x.CDifferentiableAt_rule
Proof state before:
case funProp.discharger
K✝ : Type ?u.37534
inst✝¹⁴ : RCLike K✝
X✝¹ : Type ?u.37540
inst✝¹³ : Vec K✝ X✝¹
Y✝¹ : Type ?u.37553
inst✝¹² : Vec K✝ Y✝¹
Z✝ : Type ?u.37564
inst✝¹¹ : Vec K✝ Z✝
ι✝ : Type ?u.37575
inst✝¹⁰ : IndexType ι✝
E✝ : ι✝ → Type ?u.37584
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.37600
inst✝⁸ : RCLike K
X✝ : Type ?u.37606
inst✝⁷ : Vec K X✝
Y✝ : Type ?u.37619
inst✝⁶ : Vec K Y✝
Z : Type ?u.37630
inst✝⁵ : Vec K Z
ι : Type ?u.37641
inst✝⁴ : IndexType ι
E : ι → Type ?u.37650
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
x : X
hf : CDifferentiableAt R f x
hx : f x ≠ 0
⊢ ?x ≠ 0
Tactic:
assumption
Proof state after:
no goals
Theorem: SciLean.Basis.proj.arg_x.CDifferentiable_rule
Proof state before:
K✝¹ : Type ?u.39673
inst✝²⁴ : RCLike K✝¹
X✝¹ : Type ?u.39679
inst✝²³ : Vec K✝¹ X✝¹
Y✝¹ : Type ?u.39692
inst✝²² : Vec K✝¹ Y✝¹
Z✝¹ : Type ?u.39703
inst✝²¹ : Vec K✝¹ Z✝¹
ι✝ : Type ?u.39714
inst✝²⁰ : IndexType ι✝
E✝ : ι✝ → Type ?u.39723
inst✝¹⁹ : (i : ι✝) → Vec K✝¹ (E✝ i)
K✝ : Type ?u.39739
inst✝¹⁸ : RCLike K✝
X✝ : Type ?u.39745
inst✝¹⁷ : Vec K✝ X✝
Y✝ : Type ?u.39758
inst✝¹⁶ : Vec K✝ Y✝
Z✝ : Type ?u.39769
inst✝¹⁵ : Vec K✝ Z✝
ι : Type ?u.39780
inst✝¹⁴ : IndexType ι
E : ι → Type ?u.39789
inst✝¹³ : (i : ι) → Vec K✝ (E i)
K : Type u_1
inst✝¹² : RCLike K
IX : Type u_3
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_2
inst✝⁸ : FinVec IX K X
IY : Type ?u.39902
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type ?u.39905
inst✝⁴ : FinVec IY K Y
IZ : Type ?u.39991
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.39994
inst✝ : FinVec IZ K Z
i : IX
⊢ CDifferentiable K fun x => ℼ i x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Basis.proj.arg_x.CDifferentiableAt_rule
Proof state before:
K✝¹ : Type ?u.40447
inst✝²⁴ : RCLike K✝¹
X✝¹ : Type ?u.40453
inst✝²³ : Vec K✝¹ X✝¹
Y✝¹ : Type ?u.40466
inst✝²² : Vec K✝¹ Y✝¹
Z✝¹ : Type ?u.40477
inst✝²¹ : Vec K✝¹ Z✝¹
ι✝ : Type ?u.40488
inst✝²⁰ : IndexType ι✝
E✝ : ι✝ → Type ?u.40497
inst✝¹⁹ : (i : ι✝) → Vec K✝¹ (E✝ i)
K✝ : Type ?u.40513
inst✝¹⁸ : RCLike K✝
X✝ : Type ?u.40519
inst✝¹⁷ : Vec K✝ X✝
Y✝ : Type ?u.40532
inst✝¹⁶ : Vec K✝ Y✝
Z✝ : Type ?u.40543
inst✝¹⁵ : Vec K✝ Z✝
ι : Type ?u.40554
inst✝¹⁴ : IndexType ι
E : ι → Type ?u.40563
inst✝¹³ : (i : ι) → Vec K✝ (E i)
K : Type u_1
inst✝¹² : RCLike K
IX : Type u_3
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_2
inst✝⁸ : FinVec IX K X
IY : Type ?u.40676
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type ?u.40679
inst✝⁴ : FinVec IY K Y
IZ : Type ?u.40765
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.40768
inst✝ : FinVec IZ K Z
i : IX
x : X
⊢ CDifferentiableAt K (fun x => ℼ i x) x
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.DualBasis.dualProj.arg_x.CDifferentiable_rule
Proof state before:
K✝¹ : Type ?u.41534
inst✝²⁴ : RCLike K✝¹
X✝¹ : Type ?u.41540
inst✝²³ : Vec K✝¹ X✝¹
Y✝¹ : Type ?u.41553
inst✝²² : Vec K✝¹ Y✝¹
Z✝¹ : Type ?u.41564
inst✝²¹ : Vec K✝¹ Z✝¹
ι✝ : Type ?u.41575
inst✝²⁰ : IndexType ι✝
E✝ : ι✝ → Type ?u.41584
inst✝¹⁹ : (i : ι✝) → Vec K✝¹ (E✝ i)
K✝ : Type ?u.41600
inst✝¹⁸ : RCLike K✝
X✝ : Type ?u.41606
inst✝¹⁷ : Vec K✝ X✝
Y✝ : Type ?u.41619
inst✝¹⁶ : Vec K✝ Y✝
Z✝ : Type ?u.41630
inst✝¹⁵ : Vec K✝ Z✝
ι : Type ?u.41641
inst✝¹⁴ : IndexType ι
E : ι → Type ?u.41650
inst✝¹³ : (i : ι) → Vec K✝ (E i)
K : Type u_1
inst✝¹² : RCLike K
IX : Type u_3
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_2
inst✝⁸ : FinVec IX K X
IY : Type ?u.41763
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type ?u.41766
inst✝⁴ : FinVec IY K Y
IZ : Type ?u.41852
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.41855
inst✝ : FinVec IZ K Z
i : IX
⊢ CDifferentiable K fun x => ℼ' i x
Tactic:
sorry_proof
Proof state after:
no goals