Theorems · Theorem · global analysis

HasFDerivWithinAt.lim

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul 𝕜 E] {F : Type u_3} [inst_6 : AddCommGroup F]
  [inst_7 : Module 𝕜 F] [inst_8 : TopologicalSpace F] [ContinuousAdd F] [ContinuousSMul 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {x : E} {s : Set E},
  HasFDerivWithinAt f f' s x →
    ∀ {α : Type u_4} {l : Filter α} {c : α → 𝕜} {d : α → E} {v : E},
      Filter.Tendsto d l (nhds 0) →
        (∀ᶠ (n : α) in l, x + d n ∈ s) →
          Filter.Tendsto (fun n => c n • d n) l (nhds v) →
            Filter.Tendsto (fun n => c n • (f (x + d n) - f x)) l (nhds (f' v))

If a function f has a derivative f' at x, a rescaled version of f around x converges to f', i.e., n (f (x + (1/n) v) - f x) converges to f' v. More generally, if d n tends to zero and c n * d n tends to v, then c n * (f (x + d n) - f x) tends to f' v. This lemma expresses this fact, for functions having a derivative within a set. Its specific formulation is useful for tangent cone related discussions.

Defined in

Mathlib.Analysis.Calculus.FDeriv.Basic

Cited by

4 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldAddCommGroupModuleTopologicalSpaceContinuousAddContinuousSMulAddCommGroupModuleTopologicalSpaceContinuousAddContinuousSMul