English
Uniform Cauchy sequences of derivatives remain uniform after applying the scalar operator 1 smulRight, i.e., preserving uniform convergence when scaling derivatives by 1.
Русский
Униформная последовательность производных сохраняется под действием скалярного оператора 1 smulRight, т.е. сохраняется равномерная сходимость при умножении на 1.
LaTeX
$$$\\text{If } hf' : UniformCauchySeqOnFilter f' l l', \\; \\text{then } UniformCauchySeqOnFilter (\\lambda n z. (1: \\mathbb{K} \\toL[\\mathbb{K}] \\mathbb{K}).smulRight (f' n z)) l l'.$$$
Lean4
/-- 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)` -/
theorem difference_quotients_converge_uniformly {E : Type*} [NormedAddCommGroup E] {𝕜 : Type*} [RCLike 𝕜]
[NormedSpace 𝕜 E] {G : Type*} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : ι → E → G} {g : E → G}
{f' : ι → E → E →L[𝕜] G} {g' : E → E →L[𝕜] G} {x : E} (hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x))
(hf : ∀ᶠ n : ι × E in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2)
(hfg : ∀ᶠ y : E in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))) :
TendstoUniformlyOnFilter (fun n : ι => fun y : E => (‖y - x‖⁻¹ : 𝕜) • (f n y - f n x))
(fun y : E => (‖y - x‖⁻¹ : 𝕜) • (g y - g x)) l (𝓝 x) :=
by
let A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 _
refine
UniformCauchySeqOnFilter.tendstoUniformlyOnFilter_of_tendsto ?_
((hfg.and (eventually_const.mpr hfg.self_of_nhds)).mono fun y hy => (hy.1.sub hy.2).const_smul _)
rw [SeminormedAddGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_zero]
rw [Metric.tendstoUniformlyOnFilter_iff]
have hfg' := hf'.uniformCauchySeqOnFilter
rw [SeminormedAddGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_zero] at hfg'
rw [Metric.tendstoUniformlyOnFilter_iff] at hfg'
intro ε hε
obtain ⟨q, hqpos, hqε⟩ := exists_pos_rat_lt hε
specialize hfg' (q : ℝ) (by simp [hqpos])
have := (tendsto_swap4_prod.eventually (hf.prod_mk hf)).diag_of_prod_right
obtain ⟨a, b, c, d, e⟩ := eventually_prod_iff.1 (hfg'.and this)
obtain ⟨r, hr, hr'⟩ := Metric.nhds_basis_ball.eventually_iff.mp d
rw [eventually_prod_iff]
refine
⟨_, b, fun e : E => Metric.ball x r e, eventually_mem_set.mpr (Metric.nhds_basis_ball.mem_of_mem hr),
fun {n} hn {y} hy => ?_⟩
simp only [Pi.zero_apply, dist_zero_left]
rw [← smul_sub, norm_smul, norm_inv, RCLike.norm_coe_norm]
refine lt_of_le_of_lt ?_ hqε
by_cases hyz' : x = y; · simp [hyz', hqpos.le]
have hyz : 0 < ‖y - x‖ := by rw [norm_pos_iff]; intro hy'; exact hyz' (eq_of_sub_eq_zero hy').symm
rw [inv_mul_le_iff₀ hyz, mul_comm, sub_sub_sub_comm]
simp only [Pi.zero_apply, dist_zero_left] at e
refine
Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le
(fun y hy => ((e hn (hr' hy)).2.1.sub (e hn (hr' hy)).2.2).hasFDerivWithinAt) (fun y hy => (e hn (hr' hy)).1.le)
(convex_ball x r) (Metric.mem_ball_self hr) hy
