[GOAL]
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
s : Set β
hfu : ∀ (n : α) (x : β), x ∈ s → ‖f n x‖ ≤ u n
⊢ TendstoUniformlyOn (fun t x => ∑ n in t, f n x) (fun x => ∑' (n : α), f n x) atTop s
[PROOFSTEP]
refine' tendstoUniformlyOn_iff.2 fun ε εpos => _
[GOAL]
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
s : Set β
hfu : ∀ (n : α) (x : β), x ∈ s → ‖f n x‖ ≤ u n
ε : ℝ
εpos : ε > 0
⊢ ∀ᶠ (n : Finset α) in atTop, ∀ (x : β), x ∈ s → dist (∑' (n : α), f n x) (∑ n in n, f n x) < ε
[PROOFSTEP]
filter_upwards [(tendsto_order.1 (tendsto_tsum_compl_atTop_zero u)).2 _ εpos] with t ht x hx
[GOAL]
case h
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
s : Set β
hfu : ∀ (n : α) (x : β), x ∈ s → ‖f n x‖ ≤ u n
ε : ℝ
εpos : ε > 0
t : Finset α
ht : ∑' (b : { x // ¬x ∈ t }), u ↑b < ε
x : β
hx : x ∈ s
⊢ dist (∑' (n : α), f n x) (∑ n in t, f n x) < ε
[PROOFSTEP]
have A : Summable fun n => ‖f n x‖ := summable_of_nonneg_of_le (fun n => norm_nonneg _) (fun n => hfu n x hx) hu
[GOAL]
case h
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
s : Set β
hfu : ∀ (n : α) (x : β), x ∈ s → ‖f n x‖ ≤ u n
ε : ℝ
εpos : ε > 0
t : Finset α
ht : ∑' (b : { x // ¬x ∈ t }), u ↑b < ε
x : β
hx : x ∈ s
A : Summable fun n => ‖f n x‖
⊢ dist (∑' (n : α), f n x) (∑ n in t, f n x) < ε
[PROOFSTEP]
rw [dist_eq_norm, ← sum_add_tsum_subtype_compl (summable_of_summable_norm A) t, add_sub_cancel']
[GOAL]
case h
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
s : Set β
hfu : ∀ (n : α) (x : β), x ∈ s → ‖f n x‖ ≤ u n
ε : ℝ
εpos : ε > 0
t : Finset α
ht : ∑' (b : { x // ¬x ∈ t }), u ↑b < ε
x : β
hx : x ∈ s
A : Summable fun n => ‖f n x‖
⊢ ‖∑' (x_1 : { x // ¬x ∈ t }), f (↑x_1) x‖ < ε
[PROOFSTEP]
apply lt_of_le_of_lt _ ht
[GOAL]
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
s : Set β
hfu : ∀ (n : α) (x : β), x ∈ s → ‖f n x‖ ≤ u n
ε : ℝ
εpos : ε > 0
t : Finset α
ht : ∑' (b : { x // ¬x ∈ t }), u ↑b < ε
x : β
hx : x ∈ s
A : Summable fun n => ‖f n x‖
⊢ ‖∑' (x_1 : { x // ¬x ∈ t }), f (↑x_1) x‖ ≤ ∑' (b : { x // ¬x ∈ t }), u ↑b
[PROOFSTEP]
apply (norm_tsum_le_tsum_norm (A.subtype _)).trans
[GOAL]
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
s : Set β
hfu : ∀ (n : α) (x : β), x ∈ s → ‖f n x‖ ≤ u n
ε : ℝ
εpos : ε > 0
t : Finset α
ht : ∑' (b : { x // ¬x ∈ t }), u ↑b < ε
x : β
hx : x ∈ s
A : Summable fun n => ‖f n x‖
⊢ ∑' (i : ↑fun x => x ∈ t → False), ‖f (↑i) x‖ ≤ ∑' (b : { x // ¬x ∈ t }), u ↑b
[PROOFSTEP]
exact tsum_le_tsum (fun n => hfu _ _ hx) (A.subtype _) (hu.subtype _)
[GOAL]
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
hfu : ∀ (n : α) (x : β), ‖f n x‖ ≤ u n
⊢ TendstoUniformly (fun t x => ∑ n in t, f n x) (fun x => ∑' (n : α), f n x) atTop
[PROOFSTEP]
rw [← tendstoUniformlyOn_univ]
[GOAL]
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
hfu : ∀ (n : α) (x : β), ‖f n x‖ ≤ u n
⊢ TendstoUniformlyOn (fun t x => ∑ n in t, f n x) (fun x => ∑' (n : α), f n x) atTop univ
[PROOFSTEP]
exact tendstoUniformlyOn_tsum hu fun n x _ => hfu n x
[GOAL]
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : TopologicalSpace β
f : α → β → F
s : Set β
hf : ∀ (i : α), ContinuousOn (f i) s
hu : Summable u
hfu : ∀ (n : α) (x : β), x ∈ s → ‖f n x‖ ≤ u n
⊢ ContinuousOn (fun x => ∑' (n : α), f n x) s
[PROOFSTEP]
classical
refine' (tendstoUniformlyOn_tsum hu hfu).continuousOn (eventually_of_forall _)
intro t
exact continuousOn_finset_sum _ fun i _ => hf i
[GOAL]
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : TopologicalSpace β
f : α → β → F
s : Set β
hf : ∀ (i : α), ContinuousOn (f i) s
hu : Summable u
hfu : ∀ (n : α) (x : β), x ∈ s → ‖f n x‖ ≤ u n
⊢ ContinuousOn (fun x => ∑' (n : α), f n x) s
[PROOFSTEP]
refine' (tendstoUniformlyOn_tsum hu hfu).continuousOn (eventually_of_forall _)
[GOAL]
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : TopologicalSpace β
f : α → β → F
s : Set β
hf : ∀ (i : α), ContinuousOn (f i) s
hu : Summable u
hfu : ∀ (n : α) (x : β), x ∈ s → ‖f n x‖ ≤ u n
⊢ ∀ (x : Finset α), ContinuousOn (fun x_1 => ∑ n in x, f n x_1) s
[PROOFSTEP]
intro t
[GOAL]
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : TopologicalSpace β
f : α → β → F
s : Set β
hf : ∀ (i : α), ContinuousOn (f i) s
hu : Summable u
hfu : ∀ (n : α) (x : β), x ∈ s → ‖f n x‖ ≤ u n
t : Finset α
⊢ ContinuousOn (fun x => ∑ n in t, f n x) s
[PROOFSTEP]
exact continuousOn_finset_sum _ fun i _ => hf i
[GOAL]
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : TopologicalSpace β
f : α → β → F
hf : ∀ (i : α), Continuous (f i)
hu : Summable u
hfu : ∀ (n : α) (x : β), ‖f n x‖ ≤ u n
⊢ Continuous fun x => ∑' (n : α), f n x
[PROOFSTEP]
simp_rw [continuous_iff_continuousOn_univ] at hf ⊢
[GOAL]
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : TopologicalSpace β
f : α → β → F
hu : Summable u
hfu : ∀ (n : α) (x : β), ‖f n x‖ ≤ u n
hf : ∀ (i : α), ContinuousOn (f i) univ
⊢ ContinuousOn (fun x => ∑' (n : α), f n x) univ
[PROOFSTEP]
exact continuousOn_tsum hf hu fun n x _ => hfu n x
[GOAL]
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x✝ : E
N : ℕ∞
hu : Summable u
hs : IsOpen s
h's : IsPreconnected s
hf : ∀ (n : α) (x : E), x ∈ s → HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), x ∈ s → ‖f' n x‖ ≤ u n
hx₀ : x₀ ∈ s
hf0 : Summable fun x => f x x₀
x : E
hx : x ∈ s
⊢ Summable fun n => f n x
[PROOFSTEP]
rw [summable_iff_cauchySeq_finset] at hf0 ⊢
[GOAL]
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x✝ : E
N : ℕ∞
hu : Summable u
hs : IsOpen s
h's : IsPreconnected s
hf : ∀ (n : α) (x : E), x ∈ s → HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), x ∈ s → ‖f' n x‖ ≤ u n
hx₀ : x₀ ∈ s
hf0 : CauchySeq fun s => ∑ b in s, f b x₀
x : E
hx : x ∈ s
⊢ CauchySeq fun s => ∑ b in s, f b x
[PROOFSTEP]
have A : UniformCauchySeqOn (fun t : Finset α => fun x => ∑ i in t, f' i x) atTop s :=
  (tendstoUniformlyOn_tsum hu hf').uniformCauchySeqOn
[GOAL]
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x✝ : E
N : ℕ∞
hu : Summable u
hs : IsOpen s
h's : IsPreconnected s
hf : ∀ (n : α) (x : E), x ∈ s → HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), x ∈ s → ‖f' n x‖ ≤ u n
hx₀ : x₀ ∈ s
hf0 : CauchySeq fun s => ∑ b in s, f b x₀
x : E
hx : x ∈ s
A : UniformCauchySeqOn (fun t x => ∑ i in t, f' i x) atTop s
⊢ CauchySeq fun s => ∑ b in s, f b x
[PROOFSTEP]
refine cauchy_map_of_uniformCauchySeqOn_fderiv (f := fun t x ↦ ∑ i in t, f i x) hs h's A (fun t y hy => ?_) hx₀ hx hf0
[GOAL]
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x✝ : E
N : ℕ∞
hu : Summable u
hs : IsOpen s
h's : IsPreconnected s
hf : ∀ (n : α) (x : E), x ∈ s → HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), x ∈ s → ‖f' n x‖ ≤ u n
hx₀ : x₀ ∈ s
hf0 : CauchySeq fun s => ∑ b in s, f b x₀
x : E
hx : x ∈ s
A : UniformCauchySeqOn (fun t x => ∑ i in t, f' i x) atTop s
t : Finset α
y : E
hy : y ∈ s
⊢ HasFDerivAt ((fun t x => ∑ i in t, f i x) t) (∑ i in t, f' i y) y
[PROOFSTEP]
exact HasFDerivAt.sum fun i _ => hf i y hy
[GOAL]
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x : E
N : ℕ∞
hu : Summable u
hs : IsOpen s
h's : IsPreconnected s
hf : ∀ (n : α) (x : E), x ∈ s → HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), x ∈ s → ‖f' n x‖ ≤ u n
hx₀ : x₀ ∈ s
hf0 : Summable fun n => f n x₀
hx : x ∈ s
⊢ HasFDerivAt (fun y => ∑' (n : α), f n y) (∑' (n : α), f' n x) x
[PROOFSTEP]
classical
have A : ∀ x : E, x ∈ s → Tendsto (fun t : Finset α => ∑ n in t, f n x) atTop (𝓝 (∑' n, f n x)) :=
  by
  intro y hy
  apply Summable.hasSum
  exact summable_of_summable_hasFDerivAt_of_isPreconnected hu hs h's hf hf' hx₀ hf0 hy
refine hasFDerivAt_of_tendstoUniformlyOn hs (tendstoUniformlyOn_tsum hu hf') (fun t y hy => ?_) A _ hx
exact HasFDerivAt.sum fun n _ => hf n y hy
[GOAL]
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x : E
N : ℕ∞
hu : Summable u
hs : IsOpen s
h's : IsPreconnected s
hf : ∀ (n : α) (x : E), x ∈ s → HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), x ∈ s → ‖f' n x‖ ≤ u n
hx₀ : x₀ ∈ s
hf0 : Summable fun n => f n x₀
hx : x ∈ s
⊢ HasFDerivAt (fun y => ∑' (n : α), f n y) (∑' (n : α), f' n x) x
[PROOFSTEP]
have A : ∀ x : E, x ∈ s → Tendsto (fun t : Finset α => ∑ n in t, f n x) atTop (𝓝 (∑' n, f n x)) :=
  by
  intro y hy
  apply Summable.hasSum
  exact summable_of_summable_hasFDerivAt_of_isPreconnected hu hs h's hf hf' hx₀ hf0 hy
[GOAL]
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x : E
N : ℕ∞
hu : Summable u
hs : IsOpen s
h's : IsPreconnected s
hf : ∀ (n : α) (x : E), x ∈ s → HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), x ∈ s → ‖f' n x‖ ≤ u n
hx₀ : x₀ ∈ s
hf0 : Summable fun n => f n x₀
hx : x ∈ s
⊢ ∀ (x : E), x ∈ s → Tendsto (fun t => ∑ n in t, f n x) atTop (𝓝 (∑' (n : α), f n x))
[PROOFSTEP]
intro y hy
[GOAL]
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x : E
N : ℕ∞
hu : Summable u
hs : IsOpen s
h's : IsPreconnected s
hf : ∀ (n : α) (x : E), x ∈ s → HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), x ∈ s → ‖f' n x‖ ≤ u n
hx₀ : x₀ ∈ s
hf0 : Summable fun n => f n x₀
hx : x ∈ s
y : E
hy : y ∈ s
⊢ Tendsto (fun t => ∑ n in t, f n y) atTop (𝓝 (∑' (n : α), f n y))
[PROOFSTEP]
apply Summable.hasSum
[GOAL]
case ha
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x : E
N : ℕ∞
hu : Summable u
hs : IsOpen s
h's : IsPreconnected s
hf : ∀ (n : α) (x : E), x ∈ s → HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), x ∈ s → ‖f' n x‖ ≤ u n
hx₀ : x₀ ∈ s
hf0 : Summable fun n => f n x₀
hx : x ∈ s
y : E
hy : y ∈ s
⊢ Summable fun b => f b y
[PROOFSTEP]
exact summable_of_summable_hasFDerivAt_of_isPreconnected hu hs h's hf hf' hx₀ hf0 hy
[GOAL]
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x : E
N : ℕ∞
hu : Summable u
hs : IsOpen s
h's : IsPreconnected s
hf : ∀ (n : α) (x : E), x ∈ s → HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), x ∈ s → ‖f' n x‖ ≤ u n
hx₀ : x₀ ∈ s
hf0 : Summable fun n => f n x₀
hx : x ∈ s
A : ∀ (x : E), x ∈ s → Tendsto (fun t => ∑ n in t, f n x) atTop (𝓝 (∑' (n : α), f n x))
⊢ HasFDerivAt (fun y => ∑' (n : α), f n y) (∑' (n : α), f' n x) x
[PROOFSTEP]
refine hasFDerivAt_of_tendstoUniformlyOn hs (tendstoUniformlyOn_tsum hu hf') (fun t y hy => ?_) A _ hx
[GOAL]
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x : E
N : ℕ∞
hu : Summable u
hs : IsOpen s
h's : IsPreconnected s
hf : ∀ (n : α) (x : E), x ∈ s → HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), x ∈ s → ‖f' n x‖ ≤ u n
hx₀ : x₀ ∈ s
hf0 : Summable fun n => f n x₀
hx : x ∈ s
A : ∀ (x : E), x ∈ s → Tendsto (fun t => ∑ n in t, f n x) atTop (𝓝 (∑' (n : α), f n x))
t : Finset α
y : E
hy : y ∈ s
⊢ HasFDerivAt (fun x => ∑ n in t, f n x) (∑ n in t, f' n y) y
[PROOFSTEP]
exact HasFDerivAt.sum fun n _ => hf n y hy
[GOAL]
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x✝ : E
N : ℕ∞
hu : Summable u
hf : ∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), ‖f' n x‖ ≤ u n
hf0 : Summable fun n => f n x₀
x : E
⊢ Summable fun n => f n x
[PROOFSTEP]
let _ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 _
[GOAL]
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x✝¹ : E
N : ℕ∞
hu : Summable u
hf : ∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), ‖f' n x‖ ≤ u n
hf0 : Summable fun n => f n x₀
x : E
x✝ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ Summable fun n => f n x
[PROOFSTEP]
exact
  summable_of_summable_hasFDerivAt_of_isPreconnected hu isOpen_univ isPreconnected_univ (fun n x _ => hf n x)
    (fun n x _ => hf' n x) (mem_univ _) hf0 (mem_univ _)
[GOAL]
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x✝ : E
N : ℕ∞
hu : Summable u
hf : ∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), ‖f' n x‖ ≤ u n
hf0 : Summable fun n => f n x₀
x : E
⊢ HasFDerivAt (fun y => ∑' (n : α), f n y) (∑' (n : α), f' n x) x
[PROOFSTEP]
let : NormedSpace ℝ E
[GOAL]
case this
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x✝ : E
N : ℕ∞
hu : Summable u
hf : ∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), ‖f' n x‖ ≤ u n
hf0 : Summable fun n => f n x₀
x : E
⊢ NormedSpace ℝ E
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x✝ : E
N : ℕ∞
hu : Summable u
hf : ∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), ‖f' n x‖ ≤ u n
hf0 : Summable fun n => f n x₀
x : E
this : NormedSpace ℝ E := ?this
⊢ HasFDerivAt (fun y => ∑' (n : α), f n y) (∑' (n : α), f' n x) x
[PROOFSTEP]
exact NormedSpace.restrictScalars ℝ 𝕜 _
[GOAL]
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x✝ : E
N : ℕ∞
hu : Summable u
hf : ∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), ‖f' n x‖ ≤ u n
hf0 : Summable fun n => f n x₀
x : E
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ HasFDerivAt (fun y => ∑' (n : α), f n y) (∑' (n : α), f' n x) x
[PROOFSTEP]
exact
  hasFDerivAt_tsum_of_isPreconnected hu isOpen_univ isPreconnected_univ (fun n x _ => hf n x) (fun n x _ => hf' n x)
    (mem_univ _) hf0 (mem_univ _)
[GOAL]
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x : E
N : ℕ∞
hu : Summable u
hf : ∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), ‖f' n x‖ ≤ u n
⊢ Differentiable 𝕜 fun y => ∑' (n : α), f n y
[PROOFSTEP]
by_cases h : ∃ x₀, Summable fun n => f n x₀
[GOAL]
case pos
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x : E
N : ℕ∞
hu : Summable u
hf : ∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), ‖f' n x‖ ≤ u n
h : ∃ x₀, Summable fun n => f n x₀
⊢ Differentiable 𝕜 fun y => ∑' (n : α), f n y
[PROOFSTEP]
rcases h with ⟨x₀, hf0⟩
[GOAL]
case pos.intro
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀✝ x : E
N : ℕ∞
hu : Summable u
hf : ∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), ‖f' n x‖ ≤ u n
x₀ : E
hf0 : Summable fun n => f n x₀
⊢ Differentiable 𝕜 fun y => ∑' (n : α), f n y
[PROOFSTEP]
intro x
[GOAL]
case pos.intro
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀✝ x✝ : E
N : ℕ∞
hu : Summable u
hf : ∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), ‖f' n x‖ ≤ u n
x₀ : E
hf0 : Summable fun n => f n x₀
x : E
⊢ DifferentiableAt 𝕜 (fun y => ∑' (n : α), f n y) x
[PROOFSTEP]
exact (hasFDerivAt_tsum hu hf hf' hf0 x).differentiableAt
[GOAL]
case neg
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x : E
N : ℕ∞
hu : Summable u
hf : ∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), ‖f' n x‖ ≤ u n
h : ¬∃ x₀, Summable fun n => f n x₀
⊢ Differentiable 𝕜 fun y => ∑' (n : α), f n y
[PROOFSTEP]
push_neg at h
[GOAL]
case neg
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x : E
N : ℕ∞
hu : Summable u
hf : ∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), ‖f' n x‖ ≤ u n
h : ∀ (x₀ : E), ¬Summable fun n => f n x₀
⊢ Differentiable 𝕜 fun y => ∑' (n : α), f n y
[PROOFSTEP]
have : (fun x => ∑' n, f n x) = 0 := by ext1 x; exact tsum_eq_zero_of_not_summable (h x)
[GOAL]
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x : E
N : ℕ∞
hu : Summable u
hf : ∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), ‖f' n x‖ ≤ u n
h : ∀ (x₀ : E), ¬Summable fun n => f n x₀
⊢ (fun x => ∑' (n : α), f n x) = 0
[PROOFSTEP]
ext1 x
[GOAL]
case h
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x✝ : E
N : ℕ∞
hu : Summable u
hf : ∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), ‖f' n x‖ ≤ u n
h : ∀ (x₀ : E), ¬Summable fun n => f n x₀
x : E
⊢ ∑' (n : α), f n x = OfNat.ofNat 0 x
[PROOFSTEP]
exact tsum_eq_zero_of_not_summable (h x)
[GOAL]
case neg
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x : E
N : ℕ∞
hu : Summable u
hf : ∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), ‖f' n x‖ ≤ u n
h : ∀ (x₀ : E), ¬Summable fun n => f n x₀
this : (fun x => ∑' (n : α), f n x) = 0
⊢ Differentiable 𝕜 fun y => ∑' (n : α), f n y
[PROOFSTEP]
rw [this]
[GOAL]
case neg
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x : E
N : ℕ∞
hu : Summable u
hf : ∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), ‖f' n x‖ ≤ u n
h : ∀ (x₀ : E), ¬Summable fun n => f n x₀
this : (fun x => ∑' (n : α), f n x) = 0
⊢ Differentiable 𝕜 0
[PROOFSTEP]
exact differentiable_const 0
[GOAL]
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀✝ x : E
N : ℕ∞
hu : Summable u
hf : ∀ (n : α), Differentiable 𝕜 (f n)
hf' : ∀ (n : α) (x : E), ‖fderiv 𝕜 (f n) x‖ ≤ u n
x₀ : E
hf0 : Summable fun n => f n x₀
⊢ (fderiv 𝕜 fun y => ∑' (n : α), f n y) = fun x => ∑' (n : α), fderiv 𝕜 (f n) x
[PROOFSTEP]
ext1 x
[GOAL]
case h
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀✝ x✝ : E
N : ℕ∞
hu : Summable u
hf : ∀ (n : α), Differentiable 𝕜 (f n)
hf' : ∀ (n : α) (x : E), ‖fderiv 𝕜 (f n) x‖ ≤ u n
x₀ : E
hf0 : Summable fun n => f n x₀
x : E
⊢ fderiv 𝕜 (fun y => ∑' (n : α), f n y) x = ∑' (n : α), fderiv 𝕜 (f n) x
[PROOFSTEP]
exact fderiv_tsum_apply hu hf hf' hf0 x
[GOAL]
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
k : ℕ
hk : ↑k ≤ N
⊢ (iteratedFDeriv 𝕜 k fun y => ∑' (n : α), f n y) = fun x => ∑' (n : α), iteratedFDeriv 𝕜 k (f n) x
[PROOFSTEP]
induction' k with k IH
[GOAL]
case zero
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
k : ℕ
hk✝ : ↑k ≤ N
hk : ↑Nat.zero ≤ N
⊢ (iteratedFDeriv 𝕜 Nat.zero fun y => ∑' (n : α), f n y) = fun x => ∑' (n : α), iteratedFDeriv 𝕜 Nat.zero (f n) x
[PROOFSTEP]
ext1 x
[GOAL]
case zero.h
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x✝ : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
k : ℕ
hk✝ : ↑k ≤ N
hk : ↑Nat.zero ≤ N
x : E
⊢ iteratedFDeriv 𝕜 Nat.zero (fun y => ∑' (n : α), f n y) x = ∑' (n : α), iteratedFDeriv 𝕜 Nat.zero (f n) x
[PROOFSTEP]
simp_rw [iteratedFDeriv_zero_eq_comp]
[GOAL]
case zero.h
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x✝ : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
k : ℕ
hk✝ : ↑k ≤ N
hk : ↑Nat.zero ≤ N
x : E
⊢ (↑(LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F)) ∘ fun y => ∑' (n : α), f n y) x =
    ∑' (n : α), (↑(LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F)) ∘ f n) x
[PROOFSTEP]
exact (continuousMultilinearCurryFin0 𝕜 E F).symm.toContinuousLinearEquiv.map_tsum
[GOAL]
case succ
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
k✝ : ℕ
hk✝ : ↑k✝ ≤ N
k : ℕ
IH : ↑k ≤ N → (iteratedFDeriv 𝕜 k fun y => ∑' (n : α), f n y) = fun x => ∑' (n : α), iteratedFDeriv 𝕜 k (f n) x
hk : ↑(Nat.succ k) ≤ N
⊢ (iteratedFDeriv 𝕜 (Nat.succ k) fun y => ∑' (n : α), f n y) = fun x =>
    ∑' (n : α), iteratedFDeriv 𝕜 (Nat.succ k) (f n) x
[PROOFSTEP]
have h'k : (k : ℕ∞) < N := lt_of_lt_of_le (WithTop.coe_lt_coe.2 (Nat.lt_succ_self _)) hk
[GOAL]
case succ
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
k✝ : ℕ
hk✝ : ↑k✝ ≤ N
k : ℕ
IH : ↑k ≤ N → (iteratedFDeriv 𝕜 k fun y => ∑' (n : α), f n y) = fun x => ∑' (n : α), iteratedFDeriv 𝕜 k (f n) x
hk : ↑(Nat.succ k) ≤ N
h'k : ↑k < N
⊢ (iteratedFDeriv 𝕜 (Nat.succ k) fun y => ∑' (n : α), f n y) = fun x =>
    ∑' (n : α), iteratedFDeriv 𝕜 (Nat.succ k) (f n) x
[PROOFSTEP]
have A : Summable fun n => iteratedFDeriv 𝕜 k (f n) 0 :=
  summable_of_norm_bounded (v k) (hv k h'k.le) fun n => h'f k n 0 h'k.le
[GOAL]
case succ
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
k✝ : ℕ
hk✝ : ↑k✝ ≤ N
k : ℕ
IH : ↑k ≤ N → (iteratedFDeriv 𝕜 k fun y => ∑' (n : α), f n y) = fun x => ∑' (n : α), iteratedFDeriv 𝕜 k (f n) x
hk : ↑(Nat.succ k) ≤ N
h'k : ↑k < N
A : Summable fun n => iteratedFDeriv 𝕜 k (f n) 0
⊢ (iteratedFDeriv 𝕜 (Nat.succ k) fun y => ∑' (n : α), f n y) = fun x =>
    ∑' (n : α), iteratedFDeriv 𝕜 (Nat.succ k) (f n) x
[PROOFSTEP]
simp_rw [iteratedFDeriv_succ_eq_comp_left, IH h'k.le]
[GOAL]
case succ
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
k✝ : ℕ
hk✝ : ↑k✝ ≤ N
k : ℕ
IH : ↑k ≤ N → (iteratedFDeriv 𝕜 k fun y => ∑' (n : α), f n y) = fun x => ∑' (n : α), iteratedFDeriv 𝕜 k (f n) x
hk : ↑(Nat.succ k) ≤ N
h'k : ↑k < N
A : Summable fun n => iteratedFDeriv 𝕜 k (f n) 0
⊢ (↑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F) ∘ fderiv 𝕜 fun x => ∑' (n : α), iteratedFDeriv 𝕜 k (f n) x) =
    fun x =>
    ∑' (n : α), (↑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F) ∘ fderiv 𝕜 (iteratedFDeriv 𝕜 k (f n))) x
[PROOFSTEP]
rw [fderiv_tsum (hv _ hk) (fun n => (hf n).differentiable_iteratedFDeriv h'k) _ A]
[GOAL]
case succ
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
k✝ : ℕ
hk✝ : ↑k✝ ≤ N
k : ℕ
IH : ↑k ≤ N → (iteratedFDeriv 𝕜 k fun y => ∑' (n : α), f n y) = fun x => ∑' (n : α), iteratedFDeriv 𝕜 k (f n) x
hk : ↑(Nat.succ k) ≤ N
h'k : ↑k < N
A : Summable fun n => iteratedFDeriv 𝕜 k (f n) 0
⊢ (↑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F) ∘ fun x =>
      ∑' (n : α), fderiv 𝕜 (fun x => iteratedFDeriv 𝕜 k (f n) x) x) =
    fun x =>
    ∑' (n : α), (↑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F) ∘ fderiv 𝕜 (iteratedFDeriv 𝕜 k (f n))) x
[PROOFSTEP]
ext1 x
[GOAL]
case succ.h
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x✝ : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
k✝ : ℕ
hk✝ : ↑k✝ ≤ N
k : ℕ
IH : ↑k ≤ N → (iteratedFDeriv 𝕜 k fun y => ∑' (n : α), f n y) = fun x => ∑' (n : α), iteratedFDeriv 𝕜 k (f n) x
hk : ↑(Nat.succ k) ≤ N
h'k : ↑k < N
A : Summable fun n => iteratedFDeriv 𝕜 k (f n) 0
x : E
⊢ (↑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F) ∘ fun x =>
        ∑' (n : α), fderiv 𝕜 (fun x => iteratedFDeriv 𝕜 k (f n) x) x)
      x =
    ∑' (n : α), (↑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F) ∘ fderiv 𝕜 (iteratedFDeriv 𝕜 k (f n))) x
[PROOFSTEP]
exact (continuousMultilinearCurryLeftEquiv 𝕜 (fun _ : Fin (k + 1) => E) F).toContinuousLinearEquiv.map_tsum
[GOAL]
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
k✝ : ℕ
hk✝ : ↑k✝ ≤ N
k : ℕ
IH : ↑k ≤ N → (iteratedFDeriv 𝕜 k fun y => ∑' (n : α), f n y) = fun x => ∑' (n : α), iteratedFDeriv 𝕜 k (f n) x
hk : ↑(Nat.succ k) ≤ N
h'k : ↑k < N
A : Summable fun n => iteratedFDeriv 𝕜 k (f n) 0
⊢ ∀ (n : α) (x : E), ‖fderiv 𝕜 (fun x => iteratedFDeriv 𝕜 k (f n) x) x‖ ≤ v (Nat.succ k) n
[PROOFSTEP]
intro n x
[GOAL]
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x✝ : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
k✝ : ℕ
hk✝ : ↑k✝ ≤ N
k : ℕ
IH : ↑k ≤ N → (iteratedFDeriv 𝕜 k fun y => ∑' (n : α), f n y) = fun x => ∑' (n : α), iteratedFDeriv 𝕜 k (f n) x
hk : ↑(Nat.succ k) ≤ N
h'k : ↑k < N
A : Summable fun n => iteratedFDeriv 𝕜 k (f n) 0
n : α
x : E
⊢ ‖fderiv 𝕜 (fun x => iteratedFDeriv 𝕜 k (f n) x) x‖ ≤ v (Nat.succ k) n
[PROOFSTEP]
simpa only [iteratedFDeriv_succ_eq_comp_left, LinearIsometryEquiv.norm_map, comp_apply] using h'f k.succ n x hk
[GOAL]
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x✝ : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
k : ℕ
hk : ↑k ≤ N
x : E
⊢ iteratedFDeriv 𝕜 k (fun y => ∑' (n : α), f n y) x = ∑' (n : α), iteratedFDeriv 𝕜 k (f n) x
[PROOFSTEP]
rw [iteratedFDeriv_tsum hf hv h'f hk]
[GOAL]
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
⊢ ContDiff 𝕜 N fun x => ∑' (i : α), f i x
[PROOFSTEP]
rw [contDiff_iff_continuous_differentiable]
[GOAL]
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
⊢ (∀ (m : ℕ), ↑m ≤ N → Continuous fun x => iteratedFDeriv 𝕜 m (fun x => ∑' (i : α), f i x) x) ∧
    ∀ (m : ℕ), ↑m < N → Differentiable 𝕜 fun x => iteratedFDeriv 𝕜 m (fun x => ∑' (i : α), f i x) x
[PROOFSTEP]
constructor
[GOAL]
case left
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
⊢ ∀ (m : ℕ), ↑m ≤ N → Continuous fun x => iteratedFDeriv 𝕜 m (fun x => ∑' (i : α), f i x) x
[PROOFSTEP]
intro m hm
[GOAL]
case left
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m ≤ N
⊢ Continuous fun x => iteratedFDeriv 𝕜 m (fun x => ∑' (i : α), f i x) x
[PROOFSTEP]
rw [iteratedFDeriv_tsum hf hv h'f hm]
[GOAL]
case left
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m ≤ N
⊢ Continuous fun x => (fun x => ∑' (n : α), iteratedFDeriv 𝕜 m (f n) x) x
[PROOFSTEP]
refine' continuous_tsum _ (hv m hm) _
[GOAL]
case left.refine'_1
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m ≤ N
⊢ ∀ (i : α), Continuous fun x => iteratedFDeriv 𝕜 m (f i) x
[PROOFSTEP]
intro i
[GOAL]
case left.refine'_1
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m ≤ N
i : α
⊢ Continuous fun x => iteratedFDeriv 𝕜 m (f i) x
[PROOFSTEP]
exact ContDiff.continuous_iteratedFDeriv hm (hf i)
[GOAL]
case left.refine'_2
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m ≤ N
⊢ ∀ (n : α) (x : E), ‖iteratedFDeriv 𝕜 m (f n) x‖ ≤ v m n
[PROOFSTEP]
intro n x
[GOAL]
case left.refine'_2
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x✝ : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m ≤ N
n : α
x : E
⊢ ‖iteratedFDeriv 𝕜 m (f n) x‖ ≤ v m n
[PROOFSTEP]
exact h'f _ _ _ hm
[GOAL]
case right
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
⊢ ∀ (m : ℕ), ↑m < N → Differentiable 𝕜 fun x => iteratedFDeriv 𝕜 m (fun x => ∑' (i : α), f i x) x
[PROOFSTEP]
intro m hm
[GOAL]
case right
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m < N
⊢ Differentiable 𝕜 fun x => iteratedFDeriv 𝕜 m (fun x => ∑' (i : α), f i x) x
[PROOFSTEP]
have h'm : ((m + 1 : ℕ) : ℕ∞) ≤ N := by
  simpa only [ENat.coe_add, Nat.cast_withBot, ENat.coe_one] using ENat.add_one_le_of_lt hm
[GOAL]
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m < N
⊢ ↑(m + 1) ≤ N
[PROOFSTEP]
simpa only [ENat.coe_add, Nat.cast_withBot, ENat.coe_one] using ENat.add_one_le_of_lt hm
[GOAL]
case right
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m < N
h'm : ↑(m + 1) ≤ N
⊢ Differentiable 𝕜 fun x => iteratedFDeriv 𝕜 m (fun x => ∑' (i : α), f i x) x
[PROOFSTEP]
rw [iteratedFDeriv_tsum hf hv h'f hm.le]
[GOAL]
case right
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m < N
h'm : ↑(m + 1) ≤ N
⊢ Differentiable 𝕜 fun x => (fun x => ∑' (n : α), iteratedFDeriv 𝕜 m (f n) x) x
[PROOFSTEP]
have A : ∀ n x, HasFDerivAt (iteratedFDeriv 𝕜 m (f n)) (fderiv 𝕜 (iteratedFDeriv 𝕜 m (f n)) x) x := fun n x =>
  (ContDiff.differentiable_iteratedFDeriv hm (hf n)).differentiableAt.hasFDerivAt
[GOAL]
case right
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m < N
h'm : ↑(m + 1) ≤ N
A : ∀ (n : α) (x : E), HasFDerivAt (iteratedFDeriv 𝕜 m (f n)) (fderiv 𝕜 (iteratedFDeriv 𝕜 m (f n)) x) x
⊢ Differentiable 𝕜 fun x => (fun x => ∑' (n : α), iteratedFDeriv 𝕜 m (f n) x) x
[PROOFSTEP]
refine differentiable_tsum (hv _ h'm) A fun n x => ?_
[GOAL]
case right
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x✝ : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m < N
h'm : ↑(m + 1) ≤ N
A : ∀ (n : α) (x : E), HasFDerivAt (iteratedFDeriv 𝕜 m (f n)) (fderiv 𝕜 (iteratedFDeriv 𝕜 m (f n)) x) x
n : α
x : E
⊢ ‖fderiv 𝕜 (iteratedFDeriv 𝕜 m (f n)) x‖ ≤ v (m + 1) n
[PROOFSTEP]
rw [fderiv_iteratedFDeriv, comp_apply, LinearIsometryEquiv.norm_map]
[GOAL]
case right
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x✝ : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m < N
h'm : ↑(m + 1) ≤ N
A : ∀ (n : α) (x : E), HasFDerivAt (iteratedFDeriv 𝕜 m (f n)) (fderiv 𝕜 (iteratedFDeriv 𝕜 m (f n)) x) x
n : α
x : E
⊢ ‖iteratedFDeriv 𝕜 (m + 1) (f n) x‖ ≤ v (m + 1) n
[PROOFSTEP]
exact h'f _ _ _ h'm
[GOAL]
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ), ↑k ≤ N → ∀ᶠ (i : α) in cofinite, ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
⊢ ContDiff 𝕜 N fun x => ∑' (i : α), f i x
[PROOFSTEP]
classical
refine contDiff_iff_forall_nat_le.2 fun m hm => ?_
let t : Set α := {i : α | ¬∀ k : ℕ, k ∈ Finset.range (m + 1) → ∀ x, ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i}
have ht : Set.Finite t :=
  haveI A :
    ∀ᶠ i in (Filter.cofinite : Filter α),
      ∀ k : ℕ, k ∈ Finset.range (m + 1) → ∀ x : E, ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i :=
    by
    rw [eventually_all_finset]
    intro i hi
    apply h'f
    simp only [Finset.mem_range_succ_iff] at hi
    exact (WithTop.coe_le_coe.2 hi).trans hm
  eventually_cofinite.2 A
let T : Finset α := ht.toFinset
have : (fun x => ∑' i, f i x) = (fun x => ∑ i in T, f i x) + fun x => ∑' i : { i // i ∉ T }, f i x :=
  by
  ext1 x
  refine' (sum_add_tsum_subtype_compl _ T).symm
  refine' summable_of_norm_bounded_eventually _ (hv 0 (zero_le _)) _
  filter_upwards [h'f 0 (zero_le _)] with i hi
  simpa only [norm_iteratedFDeriv_zero] using hi x
rw [this]
apply (ContDiff.sum fun i _ => (hf i).of_le hm).add
have h'u : ∀ k : ℕ, (k : ℕ∞) ≤ m → Summable (v k ∘ ((↑) : { i // i ∉ T } → α)) := fun k hk =>
  (hv k (hk.trans hm)).subtype _
refine' contDiff_tsum (fun i => (hf i).of_le hm) h'u _
rintro k ⟨i, hi⟩ x hk
dsimp
simp only [Finite.mem_toFinset, mem_setOf_eq, Finset.mem_range, not_forall, not_le, exists_prop, not_exists, not_and,
  not_lt] at hi
exact hi k (Nat.lt_succ_iff.2 (WithTop.coe_le_coe.1 hk)) x
[GOAL]
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ), ↑k ≤ N → ∀ᶠ (i : α) in cofinite, ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
⊢ ContDiff 𝕜 N fun x => ∑' (i : α), f i x
[PROOFSTEP]
refine contDiff_iff_forall_nat_le.2 fun m hm => ?_
[GOAL]
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ), ↑k ≤ N → ∀ᶠ (i : α) in cofinite, ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m ≤ N
⊢ ContDiff 𝕜 ↑m fun x => ∑' (i : α), f i x
[PROOFSTEP]
let t : Set α := {i : α | ¬∀ k : ℕ, k ∈ Finset.range (m + 1) → ∀ x, ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i}
[GOAL]
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ), ↑k ≤ N → ∀ᶠ (i : α) in cofinite, ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m ≤ N
t : Set α := {i | ¬∀ (k : ℕ), k ∈ Finset.range (m + 1) → ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i}
⊢ ContDiff 𝕜 ↑m fun x => ∑' (i : α), f i x
[PROOFSTEP]
have ht : Set.Finite t :=
  haveI A :
    ∀ᶠ i in (Filter.cofinite : Filter α),
      ∀ k : ℕ, k ∈ Finset.range (m + 1) → ∀ x : E, ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i :=
    by
    rw [eventually_all_finset]
    intro i hi
    apply h'f
    simp only [Finset.mem_range_succ_iff] at hi
    exact (WithTop.coe_le_coe.2 hi).trans hm
  eventually_cofinite.2 A
[GOAL]
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ), ↑k ≤ N → ∀ᶠ (i : α) in cofinite, ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m ≤ N
t : Set α := {i | ¬∀ (k : ℕ), k ∈ Finset.range (m + 1) → ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i}
⊢ ∀ᶠ (i : α) in cofinite, ∀ (k : ℕ), k ∈ Finset.range (m + 1) → ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
[PROOFSTEP]
rw [eventually_all_finset]
[GOAL]
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ), ↑k ≤ N → ∀ᶠ (i : α) in cofinite, ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m ≤ N
t : Set α := {i | ¬∀ (k : ℕ), k ∈ Finset.range (m + 1) → ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i}
⊢ ∀ (i : ℕ), i ∈ Finset.range (m + 1) → ∀ᶠ (x : α) in cofinite, ∀ (x_1 : E), ‖iteratedFDeriv 𝕜 i (f x) x_1‖ ≤ v i x
[PROOFSTEP]
intro i hi
[GOAL]
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ), ↑k ≤ N → ∀ᶠ (i : α) in cofinite, ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m ≤ N
t : Set α := {i | ¬∀ (k : ℕ), k ∈ Finset.range (m + 1) → ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i}
i : ℕ
hi : i ∈ Finset.range (m + 1)
⊢ ∀ᶠ (x : α) in cofinite, ∀ (x_1 : E), ‖iteratedFDeriv 𝕜 i (f x) x_1‖ ≤ v i x
[PROOFSTEP]
apply h'f
[GOAL]
case a
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ), ↑k ≤ N → ∀ᶠ (i : α) in cofinite, ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m ≤ N
t : Set α := {i | ¬∀ (k : ℕ), k ∈ Finset.range (m + 1) → ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i}
i : ℕ
hi : i ∈ Finset.range (m + 1)
⊢ ↑i ≤ N
[PROOFSTEP]
simp only [Finset.mem_range_succ_iff] at hi
[GOAL]
case a
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ), ↑k ≤ N → ∀ᶠ (i : α) in cofinite, ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m ≤ N
t : Set α := {i | ¬∀ (k : ℕ), k ∈ Finset.range (m + 1) → ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i}
i : ℕ
hi : i ≤ m
⊢ ↑i ≤ N
[PROOFSTEP]
exact (WithTop.coe_le_coe.2 hi).trans hm
[GOAL]
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ), ↑k ≤ N → ∀ᶠ (i : α) in cofinite, ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m ≤ N
t : Set α := {i | ¬∀ (k : ℕ), k ∈ Finset.range (m + 1) → ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i}
ht : Set.Finite t
⊢ ContDiff 𝕜 ↑m fun x => ∑' (i : α), f i x
[PROOFSTEP]
let T : Finset α := ht.toFinset
[GOAL]
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ), ↑k ≤ N → ∀ᶠ (i : α) in cofinite, ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m ≤ N
t : Set α := {i | ¬∀ (k : ℕ), k ∈ Finset.range (m + 1) → ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i}
ht : Set.Finite t
T : Finset α := Finite.toFinset ht
⊢ ContDiff 𝕜 ↑m fun x => ∑' (i : α), f i x
[PROOFSTEP]
have : (fun x => ∑' i, f i x) = (fun x => ∑ i in T, f i x) + fun x => ∑' i : { i // i ∉ T }, f i x :=
  by
  ext1 x
  refine' (sum_add_tsum_subtype_compl _ T).symm
  refine' summable_of_norm_bounded_eventually _ (hv 0 (zero_le _)) _
  filter_upwards [h'f 0 (zero_le _)] with i hi
  simpa only [norm_iteratedFDeriv_zero] using hi x
[GOAL]
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ), ↑k ≤ N → ∀ᶠ (i : α) in cofinite, ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m ≤ N
t : Set α := {i | ¬∀ (k : ℕ), k ∈ Finset.range (m + 1) → ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i}
ht : Set.Finite t
T : Finset α := Finite.toFinset ht
⊢ (fun x => ∑' (i : α), f i x) = (fun x => ∑ i in T, f i x) + fun x => ∑' (i : { i // ¬i ∈ T }), f (↑i) x
[PROOFSTEP]
ext1 x
[GOAL]
case h
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x✝ : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ), ↑k ≤ N → ∀ᶠ (i : α) in cofinite, ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m ≤ N
t : Set α := {i | ¬∀ (k : ℕ), k ∈ Finset.range (m + 1) → ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i}
ht : Set.Finite t
T : Finset α := Finite.toFinset ht
x : E
⊢ ∑' (i : α), f i x = ((fun x => ∑ i in T, f i x) + fun x => ∑' (i : { i // ¬i ∈ T }), f (↑i) x) x
[PROOFSTEP]
refine' (sum_add_tsum_subtype_compl _ T).symm
[GOAL]
case h
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x✝ : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ), ↑k ≤ N → ∀ᶠ (i : α) in cofinite, ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m ≤ N
t : Set α := {i | ¬∀ (k : ℕ), k ∈ Finset.range (m + 1) → ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i}
ht : Set.Finite t
T : Finset α := Finite.toFinset ht
x : E
⊢ Summable fun i => f i x
[PROOFSTEP]
refine' summable_of_norm_bounded_eventually _ (hv 0 (zero_le _)) _
[GOAL]
case h
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x✝ : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ), ↑k ≤ N → ∀ᶠ (i : α) in cofinite, ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m ≤ N
t : Set α := {i | ¬∀ (k : ℕ), k ∈ Finset.range (m + 1) → ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i}
ht : Set.Finite t
T : Finset α := Finite.toFinset ht
x : E
⊢ ∀ᶠ (i : α) in cofinite, ‖f i x‖ ≤ v 0 i
[PROOFSTEP]
filter_upwards [h'f 0 (zero_le _)] with i hi
[GOAL]
case h
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x✝ : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ), ↑k ≤ N → ∀ᶠ (i : α) in cofinite, ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m ≤ N
t : Set α := {i | ¬∀ (k : ℕ), k ∈ Finset.range (m + 1) → ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i}
ht : Set.Finite t
T : Finset α := Finite.toFinset ht
x : E
i : α
hi : ∀ (x : E), ‖iteratedFDeriv 𝕜 0 (f i) x‖ ≤ v 0 i
⊢ ‖f i x‖ ≤ v 0 i
[PROOFSTEP]
simpa only [norm_iteratedFDeriv_zero] using hi x
[GOAL]
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ), ↑k ≤ N → ∀ᶠ (i : α) in cofinite, ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m ≤ N
t : Set α := {i | ¬∀ (k : ℕ), k ∈ Finset.range (m + 1) → ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i}
ht : Set.Finite t
T : Finset α := Finite.toFinset ht
this : (fun x => ∑' (i : α), f i x) = (fun x => ∑ i in T, f i x) + fun x => ∑' (i : { i // ¬i ∈ T }), f (↑i) x
⊢ ContDiff 𝕜 ↑m fun x => ∑' (i : α), f i x
[PROOFSTEP]
rw [this]
[GOAL]
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ), ↑k ≤ N → ∀ᶠ (i : α) in cofinite, ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m ≤ N
t : Set α := {i | ¬∀ (k : ℕ), k ∈ Finset.range (m + 1) → ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i}
ht : Set.Finite t
T : Finset α := Finite.toFinset ht
this : (fun x => ∑' (i : α), f i x) = (fun x => ∑ i in T, f i x) + fun x => ∑' (i : { i // ¬i ∈ T }), f (↑i) x
⊢ ContDiff 𝕜 (↑m) ((fun x => ∑ i in T, f i x) + fun x => ∑' (i : { i // ¬i ∈ T }), f (↑i) x)
[PROOFSTEP]
apply (ContDiff.sum fun i _ => (hf i).of_le hm).add
[GOAL]
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ), ↑k ≤ N → ∀ᶠ (i : α) in cofinite, ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m ≤ N
t : Set α := {i | ¬∀ (k : ℕ), k ∈ Finset.range (m + 1) → ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i}
ht : Set.Finite t
T : Finset α := Finite.toFinset ht
this : (fun x => ∑' (i : α), f i x) = (fun x => ∑ i in T, f i x) + fun x => ∑' (i : { i // ¬i ∈ T }), f (↑i) x
⊢ ContDiff 𝕜 ↑m fun x => (fun x => ∑' (i : { i // ¬i ∈ T }), f (↑i) x) x
[PROOFSTEP]
have h'u : ∀ k : ℕ, (k : ℕ∞) ≤ m → Summable (v k ∘ ((↑) : { i // i ∉ T } → α)) := fun k hk =>
  (hv k (hk.trans hm)).subtype _
[GOAL]
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ), ↑k ≤ N → ∀ᶠ (i : α) in cofinite, ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m ≤ N
t : Set α := {i | ¬∀ (k : ℕ), k ∈ Finset.range (m + 1) → ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i}
ht : Set.Finite t
T : Finset α := Finite.toFinset ht
this : (fun x => ∑' (i : α), f i x) = (fun x => ∑ i in T, f i x) + fun x => ∑' (i : { i // ¬i ∈ T }), f (↑i) x
h'u : ∀ (k : ℕ), ↑k ≤ ↑m → Summable (v k ∘ Subtype.val)
⊢ ContDiff 𝕜 ↑m fun x => (fun x => ∑' (i : { i // ¬i ∈ T }), f (↑i) x) x
[PROOFSTEP]
refine' contDiff_tsum (fun i => (hf i).of_le hm) h'u _
[GOAL]
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ), ↑k ≤ N → ∀ᶠ (i : α) in cofinite, ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m ≤ N
t : Set α := {i | ¬∀ (k : ℕ), k ∈ Finset.range (m + 1) → ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i}
ht : Set.Finite t
T : Finset α := Finite.toFinset ht
this : (fun x => ∑' (i : α), f i x) = (fun x => ∑ i in T, f i x) + fun x => ∑' (i : { i // ¬i ∈ T }), f (↑i) x
h'u : ∀ (k : ℕ), ↑k ≤ ↑m → Summable (v k ∘ Subtype.val)
⊢ ∀ (k : ℕ) (i : { i // ¬i ∈ T }) (x : E), ↑k ≤ ↑m → ‖iteratedFDeriv 𝕜 k (fun x => f (↑i) x) x‖ ≤ (v k ∘ Subtype.val) i
[PROOFSTEP]
rintro k ⟨i, hi⟩ x hk
[GOAL]
case mk
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x✝ : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ), ↑k ≤ N → ∀ᶠ (i : α) in cofinite, ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m ≤ N
t : Set α := {i | ¬∀ (k : ℕ), k ∈ Finset.range (m + 1) → ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i}
ht : Set.Finite t
T : Finset α := Finite.toFinset ht
this : (fun x => ∑' (i : α), f i x) = (fun x => ∑ i in T, f i x) + fun x => ∑' (i : { i // ¬i ∈ T }), f (↑i) x
h'u : ∀ (k : ℕ), ↑k ≤ ↑m → Summable (v k ∘ Subtype.val)
k : ℕ
i : α
hi : ¬i ∈ T
x : E
hk : ↑k ≤ ↑m
⊢ ‖iteratedFDeriv 𝕜 k (fun x => f (↑{ val := i, property := hi }) x) x‖ ≤
    (v k ∘ Subtype.val) { val := i, property := hi }
[PROOFSTEP]
dsimp
[GOAL]
case mk
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x✝ : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ), ↑k ≤ N → ∀ᶠ (i : α) in cofinite, ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m ≤ N
t : Set α := {i | ¬∀ (k : ℕ), k ∈ Finset.range (m + 1) → ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i}
ht : Set.Finite t
T : Finset α := Finite.toFinset ht
this : (fun x => ∑' (i : α), f i x) = (fun x => ∑ i in T, f i x) + fun x => ∑' (i : { i // ¬i ∈ T }), f (↑i) x
h'u : ∀ (k : ℕ), ↑k ≤ ↑m → Summable (v k ∘ Subtype.val)
k : ℕ
i : α
hi : ¬i ∈ T
x : E
hk : ↑k ≤ ↑m
⊢ ‖iteratedFDeriv 𝕜 k (fun x => f i x) x‖ ≤ v k i
[PROOFSTEP]
simp only [Finite.mem_toFinset, mem_setOf_eq, Finset.mem_range, not_forall, not_le, exists_prop, not_exists, not_and,
  not_lt] at hi
[GOAL]
case mk
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x✝ : E
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 N (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ), ↑k ≤ N → ∀ᶠ (i : α) in cofinite, ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m ≤ N
t : Set α := {i | ¬∀ (k : ℕ), k ∈ Finset.range (m + 1) → ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i}
ht : Set.Finite t
T : Finset α := Finite.toFinset ht
this : (fun x => ∑' (i : α), f i x) = (fun x => ∑ i in T, f i x) + fun x => ∑' (i : { i // ¬i ∈ T }), f (↑i) x
h'u : ∀ (k : ℕ), ↑k ≤ ↑m → Summable (v k ∘ Subtype.val)
k : ℕ
i : α
x : E
hk : ↑k ≤ ↑m
hi : ∀ (x : ℕ), x < m + 1 → ∀ (x_1 : E), ‖iteratedFDeriv 𝕜 x (f i) x_1‖ ≤ v x i
⊢ ‖iteratedFDeriv 𝕜 k (fun x => f i x) x‖ ≤ v k i
[PROOFSTEP]
exact hi k (Nat.lt_succ_iff.2 (WithTop.coe_le_coe.1 hk)) x


[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
⊢ radius p = liminf (fun n => 1 / ↑(‖p n‖₊ ^ (1 / ↑n))) atTop
[PROOFSTEP]
have : ∀ (r : ℝ≥0) {n : ℕ}, 0 < n → ((r : ℝ≥0∞) ≤ 1 / ↑(‖p n‖₊ ^ (1 / (n : ℝ))) ↔ ‖p n‖₊ * r ^ n ≤ 1) :=
  by
  intro r n hn
  have : 0 < (n : ℝ) := Nat.cast_pos.2 hn
  conv_lhs =>
    rw [one_div, ENNReal.le_inv_iff_mul_le, ← ENNReal.coe_mul, ENNReal.coe_le_one_iff, one_div, ← NNReal.rpow_one r, ←
      mul_inv_cancel this.ne', NNReal.rpow_mul, ← NNReal.mul_rpow, ← NNReal.one_rpow n⁻¹,
      NNReal.rpow_le_rpow_iff (inv_pos.2 this), mul_comm, NNReal.rpow_nat_cast]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
⊢ ∀ (r : ℝ≥0) {n : ℕ}, 0 < n → (↑r ≤ 1 / ↑(‖p n‖₊ ^ (1 / ↑n)) ↔ ‖p n‖₊ * r ^ n ≤ 1)
[PROOFSTEP]
intro r n hn
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
n : ℕ
hn : 0 < n
⊢ ↑r ≤ 1 / ↑(‖p n‖₊ ^ (1 / ↑n)) ↔ ‖p n‖₊ * r ^ n ≤ 1
[PROOFSTEP]
have : 0 < (n : ℝ) := Nat.cast_pos.2 hn
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
n : ℕ
hn : 0 < n
this : 0 < ↑n
⊢ ↑r ≤ 1 / ↑(‖p n‖₊ ^ (1 / ↑n)) ↔ ‖p n‖₊ * r ^ n ≤ 1
[PROOFSTEP]
conv_lhs =>
  rw [one_div, ENNReal.le_inv_iff_mul_le, ← ENNReal.coe_mul, ENNReal.coe_le_one_iff, one_div, ← NNReal.rpow_one r, ←
    mul_inv_cancel this.ne', NNReal.rpow_mul, ← NNReal.mul_rpow, ← NNReal.one_rpow n⁻¹,
    NNReal.rpow_le_rpow_iff (inv_pos.2 this), mul_comm, NNReal.rpow_nat_cast]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
n : ℕ
hn : 0 < n
this : 0 < ↑n
| ↑r ≤ 1 / ↑(‖p n‖₊ ^ (1 / ↑n))
[PROOFSTEP]
rw [one_div, ENNReal.le_inv_iff_mul_le, ← ENNReal.coe_mul, ENNReal.coe_le_one_iff, one_div, ← NNReal.rpow_one r, ←
    mul_inv_cancel this.ne', NNReal.rpow_mul, ← NNReal.mul_rpow, ← NNReal.one_rpow n⁻¹,
    NNReal.rpow_le_rpow_iff (inv_pos.2 this), mul_comm, NNReal.rpow_nat_cast]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
n : ℕ
hn : 0 < n
this : 0 < ↑n
| ↑r ≤ 1 / ↑(‖p n‖₊ ^ (1 / ↑n))
[PROOFSTEP]
rw [one_div, ENNReal.le_inv_iff_mul_le, ← ENNReal.coe_mul, ENNReal.coe_le_one_iff, one_div, ← NNReal.rpow_one r, ←
    mul_inv_cancel this.ne', NNReal.rpow_mul, ← NNReal.mul_rpow, ← NNReal.one_rpow n⁻¹,
    NNReal.rpow_le_rpow_iff (inv_pos.2 this), mul_comm, NNReal.rpow_nat_cast]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
n : ℕ
hn : 0 < n
this : 0 < ↑n
| ↑r ≤ 1 / ↑(‖p n‖₊ ^ (1 / ↑n))
[PROOFSTEP]
rw [one_div, ENNReal.le_inv_iff_mul_le, ← ENNReal.coe_mul, ENNReal.coe_le_one_iff, one_div, ← NNReal.rpow_one r, ←
  mul_inv_cancel this.ne', NNReal.rpow_mul, ← NNReal.mul_rpow, ← NNReal.one_rpow n⁻¹,
  NNReal.rpow_le_rpow_iff (inv_pos.2 this), mul_comm, NNReal.rpow_nat_cast]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
this : ∀ (r : ℝ≥0) {n : ℕ}, 0 < n → (↑r ≤ 1 / ↑(‖p n‖₊ ^ (1 / ↑n)) ↔ ‖p n‖₊ * r ^ n ≤ 1)
⊢ radius p = liminf (fun n => 1 / ↑(‖p n‖₊ ^ (1 / ↑n))) atTop
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
this : ∀ (r : ℝ≥0) {n : ℕ}, 0 < n → (↑r ≤ 1 / ↑(‖p n‖₊ ^ (1 / ↑n)) ↔ ‖p n‖₊ * r ^ n ≤ 1)
⊢ radius p ≤ liminf (fun n => 1 / ↑(‖p n‖₊ ^ (1 / ↑n))) atTop
[PROOFSTEP]
refine' ENNReal.le_of_forall_nnreal_lt fun r hr => _
[GOAL]
case a
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
this : ∀ (r : ℝ≥0) {n : ℕ}, 0 < n → (↑r ≤ 1 / ↑(‖p n‖₊ ^ (1 / ↑n)) ↔ ‖p n‖₊ * r ^ n ≤ 1)
⊢ liminf (fun n => 1 / ↑(‖p n‖₊ ^ (1 / ↑n))) atTop ≤ radius p
[PROOFSTEP]
refine' ENNReal.le_of_forall_nnreal_lt fun r hr => _
[GOAL]
case a
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
this : ∀ (r : ℝ≥0) {n : ℕ}, 0 < n → (↑r ≤ 1 / ↑(‖p n‖₊ ^ (1 / ↑n)) ↔ ‖p n‖₊ * r ^ n ≤ 1)
r : ℝ≥0
hr : ↑r < radius p
⊢ ↑r ≤ liminf (fun n => 1 / ↑(‖p n‖₊ ^ (1 / ↑n))) atTop
[PROOFSTEP]
have := ((TFAE_exists_lt_isLittleO_pow (fun n => ‖p n‖ * r ^ n) 1).out 1 7).1 (p.isLittleO_of_lt_radius hr)
[GOAL]
case a
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
this✝ : ∀ (r : ℝ≥0) {n : ℕ}, 0 < n → (↑r ≤ 1 / ↑(‖p n‖₊ ^ (1 / ↑n)) ↔ ‖p n‖₊ * r ^ n ≤ 1)
r : ℝ≥0
hr : ↑r < radius p
this : ∃ a, a ∈ Set.Ioo 0 1 ∧ ∀ᶠ (n : ℕ) in atTop, |‖p n‖ * ↑(r ^ n)| ≤ a ^ n
⊢ ↑r ≤ liminf (fun n => 1 / ↑(‖p n‖₊ ^ (1 / ↑n))) atTop
[PROOFSTEP]
obtain ⟨a, ha, H⟩ := this
[GOAL]
case a.intro.intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
this : ∀ (r : ℝ≥0) {n : ℕ}, 0 < n → (↑r ≤ 1 / ↑(‖p n‖₊ ^ (1 / ↑n)) ↔ ‖p n‖₊ * r ^ n ≤ 1)
r : ℝ≥0
hr : ↑r < radius p
a : ℝ
ha : a ∈ Set.Ioo 0 1
H : ∀ᶠ (n : ℕ) in atTop, |‖p n‖ * ↑(r ^ n)| ≤ a ^ n
⊢ ↑r ≤ liminf (fun n => 1 / ↑(‖p n‖₊ ^ (1 / ↑n))) atTop
[PROOFSTEP]
apply le_liminf_of_le
[GOAL]
case a.intro.intro.hf
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
this : ∀ (r : ℝ≥0) {n : ℕ}, 0 < n → (↑r ≤ 1 / ↑(‖p n‖₊ ^ (1 / ↑n)) ↔ ‖p n‖₊ * r ^ n ≤ 1)
r : ℝ≥0
hr : ↑r < radius p
a : ℝ
ha : a ∈ Set.Ioo 0 1
H : ∀ᶠ (n : ℕ) in atTop, |‖p n‖ * ↑(r ^ n)| ≤ a ^ n
⊢ autoParam (IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop fun n => 1 / ↑(‖p n‖₊ ^ (1 / ↑n))) _auto✝
[PROOFSTEP]
infer_param
[GOAL]
case a.intro.intro.h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
this : ∀ (r : ℝ≥0) {n : ℕ}, 0 < n → (↑r ≤ 1 / ↑(‖p n‖₊ ^ (1 / ↑n)) ↔ ‖p n‖₊ * r ^ n ≤ 1)
r : ℝ≥0
hr : ↑r < radius p
a : ℝ
ha : a ∈ Set.Ioo 0 1
H : ∀ᶠ (n : ℕ) in atTop, |‖p n‖ * ↑(r ^ n)| ≤ a ^ n
⊢ ∀ᶠ (n : ℕ) in atTop, ↑r ≤ 1 / ↑(‖p n‖₊ ^ (1 / ↑n))
[PROOFSTEP]
rw [← eventually_map]
[GOAL]
case a.intro.intro.h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
this : ∀ (r : ℝ≥0) {n : ℕ}, 0 < n → (↑r ≤ 1 / ↑(‖p n‖₊ ^ (1 / ↑n)) ↔ ‖p n‖₊ * r ^ n ≤ 1)
r : ℝ≥0
hr : ↑r < radius p
a : ℝ
ha : a ∈ Set.Ioo 0 1
H : ∀ᶠ (n : ℕ) in atTop, |‖p n‖ * ↑(r ^ n)| ≤ a ^ n
⊢ ∀ᶠ (b : ℝ≥0∞) in map (fun n => 1 / ↑(‖p n‖₊ ^ (1 / ↑n))) atTop, ↑r ≤ b
[PROOFSTEP]
refine' H.mp ((eventually_gt_atTop 0).mono fun n hn₀ hn => (this _ hn₀).2 (NNReal.coe_le_coe.1 _))
[GOAL]
case a.intro.intro.h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
this : ∀ (r : ℝ≥0) {n : ℕ}, 0 < n → (↑r ≤ 1 / ↑(‖p n‖₊ ^ (1 / ↑n)) ↔ ‖p n‖₊ * r ^ n ≤ 1)
r : ℝ≥0
hr : ↑r < radius p
a : ℝ
ha : a ∈ Set.Ioo 0 1
H : ∀ᶠ (n : ℕ) in atTop, |‖p n‖ * ↑(r ^ n)| ≤ a ^ n
n : ℕ
hn₀ : 0 < n
hn : |‖p n‖ * ↑(r ^ n)| ≤ a ^ n
⊢ ↑(‖p n‖₊ * r ^ n) ≤ ↑1
[PROOFSTEP]
push_cast
[GOAL]
case a.intro.intro.h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
this : ∀ (r : ℝ≥0) {n : ℕ}, 0 < n → (↑r ≤ 1 / ↑(‖p n‖₊ ^ (1 / ↑n)) ↔ ‖p n‖₊ * r ^ n ≤ 1)
r : ℝ≥0
hr : ↑r < radius p
a : ℝ
ha : a ∈ Set.Ioo 0 1
H : ∀ᶠ (n : ℕ) in atTop, |‖p n‖ * ↑(r ^ n)| ≤ a ^ n
n : ℕ
hn₀ : 0 < n
hn : |‖p n‖ * ↑(r ^ n)| ≤ a ^ n
⊢ ‖p n‖ * ↑r ^ n ≤ 1
[PROOFSTEP]
exact (le_abs_self _).trans (hn.trans (pow_le_one _ ha.1.le ha.2.le))
[GOAL]
case a
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
this : ∀ (r : ℝ≥0) {n : ℕ}, 0 < n → (↑r ≤ 1 / ↑(‖p n‖₊ ^ (1 / ↑n)) ↔ ‖p n‖₊ * r ^ n ≤ 1)
r : ℝ≥0
hr : ↑r < liminf (fun n => 1 / ↑(‖p n‖₊ ^ (1 / ↑n))) atTop
⊢ ↑r ≤ radius p
[PROOFSTEP]
refine' p.le_radius_of_isBigO (IsBigO.of_bound 1 _)
[GOAL]
case a
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
this : ∀ (r : ℝ≥0) {n : ℕ}, 0 < n → (↑r ≤ 1 / ↑(‖p n‖₊ ^ (1 / ↑n)) ↔ ‖p n‖₊ * r ^ n ≤ 1)
r : ℝ≥0
hr : ↑r < liminf (fun n => 1 / ↑(‖p n‖₊ ^ (1 / ↑n))) atTop
⊢ ∀ᶠ (x : ℕ) in atTop, ‖‖p x‖ * ↑r ^ x‖ ≤ 1 * ‖1‖
[PROOFSTEP]
refine' (eventually_lt_of_lt_liminf hr).mp ((eventually_gt_atTop 0).mono fun n hn₀ hn => _)
[GOAL]
case a
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
this : ∀ (r : ℝ≥0) {n : ℕ}, 0 < n → (↑r ≤ 1 / ↑(‖p n‖₊ ^ (1 / ↑n)) ↔ ‖p n‖₊ * r ^ n ≤ 1)
r : ℝ≥0
hr : ↑r < liminf (fun n => 1 / ↑(‖p n‖₊ ^ (1 / ↑n))) atTop
n : ℕ
hn₀ : 0 < n
hn : ↑r < 1 / ↑(‖p n‖₊ ^ (1 / ↑n))
⊢ ‖‖p n‖ * ↑r ^ n‖ ≤ 1 * ‖1‖
[PROOFSTEP]
simpa using NNReal.coe_le_coe.2 ((this _ hn₀).1 hn.le)


[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x✝¹ : E
s t : Set E
L L₁ L₂ : Filter E
x✝ : E
x : E × E
⊢ 0 = ↑e x.fst - ↑e x.snd - ↑e (x.fst - x.snd)
[PROOFSTEP]
simp only [e.map_sub, sub_self]
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x✝ : E
s t : Set E
L L₁ L₂ : Filter E
x : E
⊢ 0 = ↑e x - ↑e x✝ - ↑e (x - x✝)
[PROOFSTEP]
simp only [e.map_sub, sub_self]
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderivWithin 𝕜 (↑e) s x = e
[PROOFSTEP]
rw [DifferentiableAt.fderivWithin e.differentiableAt hxs]
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderiv 𝕜 (↑e) x = e
[PROOFSTEP]
exact e.fderiv
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
h : IsBoundedLinearMap 𝕜 f
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ _root_.fderivWithin 𝕜 f s x = toContinuousLinearMap h
[PROOFSTEP]
rw [DifferentiableAt.fderivWithin h.differentiableAt hxs]
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
h : IsBoundedLinearMap 𝕜 f
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ _root_.fderiv 𝕜 f x = toContinuousLinearMap h
[PROOFSTEP]
exact h.fderiv