Theorems · Theorem · real analysis

summable_of_summable_hasFDerivAt_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 x => f x x₀) → x ∈ s → Summable fun n => f n 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 converges everywhere on the set.

Defined in

Mathlib.Analysis.Calculus.SmoothSeries

Cited by

3 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldIsRCLikeNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupCompleteSpaceNormedSpace