Theorems · Theorem · global analysis

hasFDerivAt_of_tendstoUniformlyOnFilter

∀ {ι : 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} {g : E → G} {f' : ι → E → E →L[𝕜] G}
  {g' : E → E →L[𝕜] G} {x : E} [l.NeBot],
  TendstoUniformlyOnFilter f' g' l (nhds x) →
    (∀ᶠ (n : ι × E) in l ×ˢ nhds x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2) →
      (∀ᶠ (y : E) in nhds x, Filter.Tendsto (fun n => f n y) l (nhds (g y))) → HasFDerivAt g (g' x) x

(d/dx) lim_{n → ∞} f n x = lim_{n → ∞} f' n x when the f' n converge _uniformly_ to their limit at x. In words the assumptions mean the following: * hf': The f' converge "uniformly at" x to g'. This does not mean that the f' n even converge away from x! * hf: For all (y, n) with y sufficiently close to x and n sufficiently large, f' n is the derivative of f n * hfg: The f n converge pointwise to g on a neighborhood of x

Defined in

Mathlib.Analysis.Calculus.UniformLimitsDeriv

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNontriviallyNormedFieldIsRCLikeNormedFieldNormedSpaceNormedAddCommGroupNormedSpaceFilter.NeBot