Theorems · Theorem · real analysis

hasFDerivAt_tsum

∀ {α : 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} {x₀ : E},
  Summable u →
    (∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x) →
      (∀ (n : α) (x : E), ‖f' n x‖ ≤ u n) →
        (Summable fun n => f n x₀) → ∀ (x : E), HasFDerivAt (fun y => ∑' (n : α), f n y) (∑' (n : α), f' n x) x

Consider a series of functions ∑' n, f n x. 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 and its derivative is the sum of the derivatives.

Defined in

Mathlib.Analysis.Calculus.SmoothSeries

Cited by

2 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldIsRCLikeNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupCompleteSpaceNormedSpace