Theorem: iteratedFDerivWithin_sum_apply (ForML/FDerivProd.lean)

State before:
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type u_2
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
ι : Type u_3
inst✝ : DecidableEq ι
f : ι → E → F
u : Finset ι
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
h : ∀ j ∈ u, ContDiffOn 𝕜 (↑i) (f j) s
⊢ iteratedFDerivWithin 𝕜 i (fun x => ∑ j in u, f j x) s x = ∑ j in u, iteratedFDerivWithin 𝕜 i (f j) s x
Tactic:
induction u using Finset.induction with
| empty => ext; simp [hs, hx]
| @insert a u ha IH =>
  simp only [Finset.mem_insert] at h
  simp only [Finset.mem_insert, forall_eq_or_imp] at h
  simp only [Finset.sum_insert ha]
  rw [iteratedFDerivWithin_add_apply' h.1 (ContDiffOn.sum h.2) hs hx, IH h.2]
State after:
no goals

State before:
case empty
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type u_2
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
ι : Type u_3
inst✝ : DecidableEq ι
f : ι → E → F
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
h : ∀ j ∈ ∅, ContDiffOn 𝕜 (↑i) (f j) s
⊢ iteratedFDerivWithin 𝕜 i (fun x => ∑ j in ∅, f j x) s x = ∑ j in ∅, iteratedFDerivWithin 𝕜 i (f j) s x
Tactic:
ext
State after:
case empty.H
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type u_2
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u : Set E
f✝ f₁ : E → F
g : F → G
x✝¹ x₀ : E
c : F
b : E × F → G
m n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
ι : Type u_3
inst✝ : DecidableEq ι
f : ι → E → F
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
h : ∀ j ∈ ∅, ContDiffOn 𝕜 (↑i) (f j) s
x✝ : Fin i → E
⊢ (iteratedFDerivWithin 𝕜 i (fun x => ∑ j in ∅, f j x) s x) x✝ = (∑ j in ∅, iteratedFDerivWithin 𝕜 i (f j) s x) x✝

State before:
case empty.H
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type u_2
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u : Set E
f✝ f₁ : E → F
g : F → G
x✝¹ x₀ : E
c : F
b : E × F → G
m n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
ι : Type u_3
inst✝ : DecidableEq ι
f : ι → E → F
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
h : ∀ j ∈ ∅, ContDiffOn 𝕜 (↑i) (f j) s
x✝ : Fin i → E
⊢ (iteratedFDerivWithin 𝕜 i (fun x => ∑ j in ∅, f j x) s x) x✝ = (∑ j in ∅, iteratedFDerivWithin 𝕜 i (f j) s x) x✝
Tactic:
simp [hs, hx]
State after:
no goals

State before:
case insert
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type u_2
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
ι : Type u_3
inst✝ : DecidableEq ι
f : ι → E → F
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
a : ι
u : Finset ι
ha : a ∉ u
IH :
  (∀ j ∈ u, ContDiffOn 𝕜 (↑i) (f j) s) →
    iteratedFDerivWithin 𝕜 i (fun x => ∑ j in u, f j x) s x = ∑ j in u, iteratedFDerivWithin 𝕜 i (f j) s x
h : ∀ j ∈ insert a u, ContDiffOn 𝕜 (↑i) (f j) s
⊢ iteratedFDerivWithin 𝕜 i (fun x => ∑ j in insert a u, f j x) s x =
    ∑ j in insert a u, iteratedFDerivWithin 𝕜 i (f j) s x
Tactic:
simp only [Finset.mem_insert] at h
State after:
case insert
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type u_2
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
ι : Type u_3
inst✝ : DecidableEq ι
f : ι → E → F
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
a : ι
u : Finset ι
ha : a ∉ u
IH :
  (∀ j ∈ u, ContDiffOn 𝕜 (↑i) (f j) s) →
    iteratedFDerivWithin 𝕜 i (fun x => ∑ j in u, f j x) s x = ∑ j in u, iteratedFDerivWithin 𝕜 i (f j) s x
h : ∀ (j : ι), j = a ∨ j ∈ u → ContDiffOn 𝕜 (↑i) (f j) s
⊢ iteratedFDerivWithin 𝕜 i (fun x => ∑ j in insert a u, f j x) s x =
    ∑ j in insert a u, iteratedFDerivWithin 𝕜 i (f j) s x

State before:
case insert
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type u_2
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
ι : Type u_3
inst✝ : DecidableEq ι
f : ι → E → F
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
a : ι
u : Finset ι
ha : a ∉ u
IH :
  (∀ j ∈ u, ContDiffOn 𝕜 (↑i) (f j) s) →
    iteratedFDerivWithin 𝕜 i (fun x => ∑ j in u, f j x) s x = ∑ j in u, iteratedFDerivWithin 𝕜 i (f j) s x
h : ∀ (j : ι), j = a ∨ j ∈ u → ContDiffOn 𝕜 (↑i) (f j) s
⊢ iteratedFDerivWithin 𝕜 i (fun x => ∑ j in insert a u, f j x) s x =
    ∑ j in insert a u, iteratedFDerivWithin 𝕜 i (f j) s x
Tactic:
simp only [Finset.mem_insert, forall_eq_or_imp] at h
State after:
case insert
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type u_2
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
ι : Type u_3
inst✝ : DecidableEq ι
f : ι → E → F
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
a : ι
u : Finset ι
ha : a ∉ u
IH :
  (∀ j ∈ u, ContDiffOn 𝕜 (↑i) (f j) s) →
    iteratedFDerivWithin 𝕜 i (fun x => ∑ j in u, f j x) s x = ∑ j in u, iteratedFDerivWithin 𝕜 i (f j) s x
h : ContDiffOn 𝕜 (↑i) (f a) s ∧ ∀ a ∈ u, ContDiffOn 𝕜 (↑i) (f a) s
⊢ iteratedFDerivWithin 𝕜 i (fun x => ∑ j in insert a u, f j x) s x =
    ∑ j in insert a u, iteratedFDerivWithin 𝕜 i (f j) s x

State before:
case insert
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type u_2
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
ι : Type u_3
inst✝ : DecidableEq ι
f : ι → E → F
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
a : ι
u : Finset ι
ha : a ∉ u
IH :
  (∀ j ∈ u, ContDiffOn 𝕜 (↑i) (f j) s) →
    iteratedFDerivWithin 𝕜 i (fun x => ∑ j in u, f j x) s x = ∑ j in u, iteratedFDerivWithin 𝕜 i (f j) s x
h : ContDiffOn 𝕜 (↑i) (f a) s ∧ ∀ a ∈ u, ContDiffOn 𝕜 (↑i) (f a) s
⊢ iteratedFDerivWithin 𝕜 i (fun x => ∑ j in insert a u, f j x) s x =
    ∑ j in insert a u, iteratedFDerivWithin 𝕜 i (f j) s x
Tactic:
simp only [Finset.sum_insert ha]
State after:
case insert
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type u_2
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
ι : Type u_3
inst✝ : DecidableEq ι
f : ι → E → F
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
a : ι
u : Finset ι
ha : a ∉ u
IH :
  (∀ j ∈ u, ContDiffOn 𝕜 (↑i) (f j) s) →
    iteratedFDerivWithin 𝕜 i (fun x => ∑ j in u, f j x) s x = ∑ j in u, iteratedFDerivWithin 𝕜 i (f j) s x
h : ContDiffOn 𝕜 (↑i) (f a) s ∧ ∀ a ∈ u, ContDiffOn 𝕜 (↑i) (f a) s
⊢ iteratedFDerivWithin 𝕜 i (fun x => f a x + ∑ j in u, f j x) s x =
    iteratedFDerivWithin 𝕜 i (f a) s x + ∑ j in u, iteratedFDerivWithin 𝕜 i (f j) s x

State before:
case insert
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type u_2
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
ι : Type u_3
inst✝ : DecidableEq ι
f : ι → E → F
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
a : ι
u : Finset ι
ha : a ∉ u
IH :
  (∀ j ∈ u, ContDiffOn 𝕜 (↑i) (f j) s) →
    iteratedFDerivWithin 𝕜 i (fun x => ∑ j in u, f j x) s x = ∑ j in u, iteratedFDerivWithin 𝕜 i (f j) s x
h : ContDiffOn 𝕜 (↑i) (f a) s ∧ ∀ a ∈ u, ContDiffOn 𝕜 (↑i) (f a) s
⊢ iteratedFDerivWithin 𝕜 i (fun x => f a x + ∑ j in u, f j x) s x =
    iteratedFDerivWithin 𝕜 i (f a) s x + ∑ j in u, iteratedFDerivWithin 𝕜 i (f j) s x
Tactic:
rw [iteratedFDerivWithin_add_apply' h.1 (ContDiffOn.sum h.2) hs hx, IH h.2]
State after:
no goals