Theorems · Theorem · real analysis

contDiff_tsum_of_eventually

∀ {α : 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]
  [inst_6 : NormedSpace 𝕜 F] {f : α → E → F} {v : ℕ → α → ℝ} {N : ℕ∞},
  (∀ (i : α), ContDiff 𝕜 (↑N) (f i)) →
    (∀ (k : ℕ), ↑k ≤ N → Summable (v k)) →
      (∀ (k : ℕ), ↑k ≤ N → ∀ᶠ (i : α) in Filter.cofinite, ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i) →
        ContDiff 𝕜 ↑N fun x => ∑' (i : α), f i x

Consider a series of functions ∑' i, f i x. Assume that each individual function f i is of class C^N, and moreover there is a uniform summable upper bound on the k-th derivative for each k ≤ N (except maybe for finitely many is). Then the series is also C^N.

Defined in

Mathlib.Analysis.Calculus.SmoothSeries

Cited by

1 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldIsRCLikeNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupCompleteSpaceNormedSpace