English
The sum of differentiable functions with summable bounds is differentiable on an open set.
Русский
Сумма дифференцируемых функций, ограниченных суммируемым числом, дифференцируема на открытом множестве.
LaTeX
$$$\\text{DifferentiableOn } (\\lambda w, \\sum_i F_i w)\\; U$$$
Lean4
theorem norm_cderiv_lt (hr : 0 < r) (hfM : ∀ w ∈ sphere z r, ‖f w‖ < M) (hf : ContinuousOn f (sphere z r)) :
‖cderiv r f z‖ < M / r :=
by
obtain ⟨L, hL1, hL2⟩ : ∃ L < M, ∀ w ∈ sphere z r, ‖f w‖ ≤ L :=
by
have e1 : (sphere z r).Nonempty := NormedSpace.sphere_nonempty.mpr hr.le
have e2 : ContinuousOn (fun w => ‖f w‖) (sphere z r) := continuous_norm.comp_continuousOn hf
obtain ⟨x, hx, hx'⟩ := (isCompact_sphere z r).exists_isMaxOn e1 e2
exact ⟨‖f x‖, hfM x hx, hx'⟩
exact (norm_cderiv_le hr hL2).trans_lt ((div_lt_div_iff_of_pos_right hr).mpr hL1)
