Theorems · Theorem · real analysis

hasFDerivAt_tsum_of_isPreconnected

∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedAddCommGroup F] [CompleteSpace F]
  {u : α → ℝ} [inst_6 : NormedSpace 𝕜 F] {f : α → E → F} {f' : α → E → E →L[𝕜] F} {s : Set E} {x₀ x : E},
  Summable u →
    IsOpen s →
      IsPreconnected s →
        (∀ (n : α), ∀ x ∈ s, HasFDerivAt (f n) (f' n x) x) →
          (∀ (n : α), ∀ x ∈ s, ‖f' n x‖ ≤ u n) →
            x₀ ∈ s →
              (Summable fun n => f n x₀) → x ∈ s → HasFDerivAt (fun y => ∑' (n : α), f n y) (∑' (n : α), f' n x) x

Consider a series of functions ∑' n, f n x on a preconnected open set. If the series converges at a point, and all functions in the series are differentiable with a summable bound on the derivatives, then the series is differentiable on the set and its derivative is the sum of the derivatives.

Defined in

Mathlib.Analysis.Calculus.SmoothSeries

Cited by

3 results in Mathlib

Foundations

Depth 196 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldIsRCLikeNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupCompleteSpaceNormedSpace