Theorems · Theorem · global analysis

uniformCauchySeqOn_ball_of_fderiv

∀ {ι : Type u_1} {l : Filter ι} {E : Type u_2} [inst : NormedAddCommGroup E] {𝕜 : Type u_3}
  [inst_1 : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [inst_3 : NormedSpace 𝕜 E] {G : Type u_4}
  [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace 𝕜 G] {f : ι → E → G} {f' : ι → E → E →L[𝕜] G} {x : E} {r : ℝ},
  UniformCauchySeqOn f' l (Metric.ball x r) →
    (∀ (n : ι), ∀ y ∈ Metric.ball x r, HasFDerivAt (f n) (f' n y) y) →
      Cauchy (Filter.map (fun n => f n x) l) → UniformCauchySeqOn f l (Metric.ball x r)

A variant of the second fundamental theorem of calculus (FTC-2): If a sequence of functions between real or complex normed spaces are differentiable on a ball centered at x, they form a Cauchy sequence _at_ x, and their derivatives are Cauchy uniformly on the ball, then the functions form a uniform Cauchy sequence on the ball. NOTE: The fact that we work on a ball is typically all that is necessary to work with power series and Dirichlet series (our primary use case). However, this can be generalized by replacing the ball with any connected, bounded, open set and replacing uniform convergence with local uniform convergence. See cauchy_map_of_uniformCauchySeqOn_fderiv.

Defined in

Mathlib.Analysis.Calculus.UniformLimitsDeriv

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNontriviallyNormedFieldIsRCLikeNormedFieldNormedSpaceNormedAddCommGroupNormedSpace