English
If a sequence of differentiable functions on a ball has uniformly converging derivatives and pointwise limits, then the limit function is differentiable on the ball with derivative the limit function.
Русский
Если последовательность дифференцируемых функций на шаре сходится равномерно по производным и по значениям, то предел дифференцируем на шаре и производная равна пределу производных.
LaTeX
$$$\\text{(precise HasFDerivAt conclusion from uniform limits on ball)}$$$
Lean4
theorem hasDerivAt_of_tendstoUniformlyOnFilter [NeBot l] (hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x))
(hf : ∀ᶠ n : ι × 𝕜 in l ×ˢ 𝓝 x, HasDerivAt (f n.1) (f' n.1 n.2) n.2)
(hfg : ∀ᶠ y in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))) : HasDerivAt g (g' x) x := by
-- The first part of the proof rewrites `hf` and the goal to be functions so that Lean
-- can recognize them when we apply `hasFDerivAt_of_tendstoUniformlyOnFilter`
let F' n z := (1 : 𝕜 →L[𝕜] 𝕜).smulRight (f' n z)
let G' z := (1 : 𝕜 →L[𝕜] 𝕜).smulRight (g' z)
simp_rw [hasDerivAt_iff_hasFDerivAt] at hf
⊢
-- Now we need to rewrite hf' in terms of `ContinuousLinearMap`s. The tricky part is that
-- operator norms are written in terms of `≤` whereas metrics are written in terms of `<`. So we
-- need to shrink `ε` utilizing the archimedean property of `ℝ`
have hf' : TendstoUniformlyOnFilter F' G' l (𝓝 x) :=
by
rw [Metric.tendstoUniformlyOnFilter_iff] at hf' ⊢
intro ε hε
obtain ⟨q, hq, hq'⟩ := exists_between hε.lt
apply (hf' q hq).mono
intro n hn
refine lt_of_le_of_lt ?_ hq'
simp only [dist_eq_norm] at hn ⊢
refine ContinuousLinearMap.opNorm_le_bound _ hq.le ?_
intro z
simp only [F', G', ContinuousLinearMap.coe_sub', Pi.sub_apply, ContinuousLinearMap.smulRight_apply,
ContinuousLinearMap.one_apply]
rw [← smul_sub, norm_smul, mul_comm]
gcongr
exact hasFDerivAt_of_tendstoUniformlyOnFilter hf' hf hfg
