Theorems · Theorem · real analysis

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

Consider a series of C^n functions, with summable uniform bounds on the successive derivatives. Then the iterated derivative of the sum is the sum of the iterated derivative.

Defined in

Mathlib.Analysis.Calculus.SmoothSeries

Cited by

2 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldIsRCLikeNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupCompleteSpaceNormedSpace