English
The tangent cone at a set s in a normed space E at a point x consists of all limit directions y that can be approached by sequences x + d_n with d_n→0 after scaling by some coefficients c_n with c_n→0 and c_n d_n converging to y.
Русский
В касательном коне множества s в нормированном пространстве E в точке x содержатся все пределы направлений, которыми можно приблизиться к x через последовательности x + d_n при масштабировании коэффициентами c_n → 0, так что c_n d_n → y.
LaTeX
$$$$\text{tangentConeAt}(s, x) = \{ y \mid \exists (c_n), (d_n): (\forallᶠ n, x+d_n\in s) \wedge (|c_n|) \to 0, c_n d_n \to y \}.$$$$
Lean4
/-- Consider a series of functions `∑' n, f n x`. If all functions in the series are differentiable
with a summable bound on the derivatives, then the series is differentiable.
Note that our assumptions do not ensure the pointwise convergence, but if there is no pointwise
convergence then the series is zero everywhere so the result still holds. -/
theorem differentiable_tsum (hu : Summable u) (hf : ∀ n x, HasFDerivAt (f n) (f' n x) x) (hf' : ∀ n x, ‖f' n x‖ ≤ u n) :
Differentiable 𝕜 fun y => ∑' n, f n y :=
by
by_cases h : ∃ x₀, Summable fun n => f n x₀
· rcases h with ⟨x₀, hf0⟩
intro x
exact (hasFDerivAt_tsum hu hf hf' hf0 x).differentiableAt
· push_neg at h
have : (fun x => ∑' n, f n x) = 0 := by ext1 x; exact tsum_eq_zero_of_not_summable (h x)
rw [this]
exact differentiable_const 0
