Theorems · Theorem · real analysis

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

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.

Defined in

Mathlib.Analysis.Calculus.SmoothSeries

Cited by

2 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldIsRCLikeNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupCompleteSpaceNormedSpace