English
A set has the property that the tangent directions at every point form a unique differentiable structure; equivalently, every point x in s has a unique differentiable structure around it.
Русский
Для множества выполнено свойство уникальности дифференцирования: в каждой точке x ∈ s имеется уникальная структура для дифференцирования вокруг x.
LaTeX
$$$$\mathrm{UniqueDiffOn}(s) \;:=\; \forall x\in s, \mathrm{UniqueDiffWithinAt}(\mathbb{K}, s, x).$$$$
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) (hg : ∀ n y, HasDerivAt (g n) (g' n y) y) (hg' : ∀ n y, ‖g' n y‖ ≤ u n) :
Differentiable 𝕜 fun z => ∑' n, g n z :=
by
simp_rw [hasDerivAt_iff_hasFDerivAt] at hg
refine differentiable_tsum hu hg ?_
simpa
