Theorems · Theorem · global analysis

difference_quotients_converge_uniformly

∀ {ι : Type u_1} {l : Filter ι} {E : Type u_5} [inst : NormedAddCommGroup E] {𝕜 : Type u_6} [inst_1 : RCLike 𝕜]
  [inst_2 : NormedSpace 𝕜 E] {G : Type u_7} [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] {f : ι → E → G}
  {g : E → G} {f' : ι → E → E →L[𝕜] G} {g' : E → E →L[𝕜] G} {x : E},
  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))) →
        TendstoUniformlyOnFilter (fun n y => (↑‖y - x‖)⁻¹ • (f n y - f n x)) (fun y => (↑‖y - x‖)⁻¹ • (g y - g x)) l
          (nhds x)

If f_n → g pointwise and the derivatives (f_n)' → h _uniformly_ converge, then in fact for a fixed y, the difference quotients ‖z - y‖⁻¹ • (f_n z - f_n y) converge _uniformly_ to ‖z - y‖⁻¹ • (g z - g y)

Defined in

Mathlib.Analysis.Calculus.UniformLimitsDeriv

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupRCLikeNormedSpaceNormedAddCommGroupNormedSpace