Rescaled derivative limits #
This file records the limit, in a seminormed space, obtained by sampling a differentiable map at
t / n and multiplying its value by n. The scalar field has characteristic zero and continuous
nonnegative-rational scalar multiplication, so t / n tends to zero. These assumptions hold
for both real and complex scalars.
Main result #
tendsto_nsmul_apply_div_of_hasDerivAt: a map sending zero to zero with derivativef'satisfiesn • f (t / n) → t • f'.
theorem
tendsto_nsmul_apply_div_of_hasDerivAt
{𝕜 : Type u_1}
{F : Type u_2}
[NontriviallyNormedField 𝕜]
[CharZero 𝕜]
[ContinuousSMul ℚ≥0 𝕜]
[SeminormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : 𝕜 → F}
{f' : F}
(hf : HasDerivAt f f' 0)
(hf0 : f 0 = 0)
(t : 𝕜)
:
Filter.Tendsto (fun (n : ℕ) => n • f (t / ↑n)) Filter.atTop (nhds (t • f'))
If f passes through zero with derivative f', then n • f (t / n) tends to t • f'.