English
If t is dense in s, the range of derivWithin is contained in the closure of the span of f '' t.
Русский
Если t плотно входит в s, образ производной внутри s лежит в замыкании линейной оболочки образа t.
LaTeX
$$$\\mathrm{range}(\\mathrm{derivWithin} f s) \\subseteq \\overline{\\mathrm{span}(f''t)}$$$
Lean4
/-- Given a set `t` such that `s ∩ t` is dense in `s`, then the range of `derivWithin f s` is
contained in the closure of the submodule spanned by the image of `t`. -/
theorem range_derivWithin_subset_closure_span_image (f : 𝕜 → F) {s t : Set 𝕜} (h : s ⊆ closure (s ∩ t)) :
range (derivWithin f s) ⊆ closure (Submodule.span 𝕜 (f '' t)) :=
by
rintro - ⟨x, rfl⟩
by_cases H : UniqueDiffWithinAt 𝕜 s x; swap
· simpa [derivWithin_zero_of_not_uniqueDiffWithinAt H] using subset_closure (zero_mem _)
by_cases H' : DifferentiableWithinAt 𝕜 f s x; swap
· rw [derivWithin_zero_of_not_differentiableWithinAt H']
exact subset_closure (zero_mem _)
have I : (𝓝[(s ∩ t) \ { x }] x).NeBot :=
by
rw [← accPt_principal_iff_nhdsWithin, ← uniqueDiffWithinAt_iff_accPt]
exact H.mono_closure h
have : Tendsto (slope f x) (𝓝[(s ∩ t) \ { x }] x) (𝓝 (derivWithin f s x)) :=
by
apply Tendsto.mono_left (hasDerivWithinAt_iff_tendsto_slope.1 H'.hasDerivWithinAt)
rw [inter_comm, inter_diff_assoc]
exact nhdsWithin_mono _ inter_subset_right
rw [← closure_closure, ← Submodule.topologicalClosure_coe]
apply mem_closure_of_tendsto this
filter_upwards [self_mem_nhdsWithin] with y hy
simp only [slope, vsub_eq_sub, SetLike.mem_coe]
refine Submodule.smul_mem _ _ (Submodule.sub_mem _ ?_ ?_)
· apply Submodule.le_topologicalClosure
apply Submodule.subset_span
exact mem_image_of_mem _ hy.1.2
· apply Submodule.closure_subset_topologicalClosure_span
suffices A : f x ∈ closure (f '' (s ∩ t)) from closure_mono (image_mono inter_subset_right) A
apply ContinuousWithinAt.mem_closure_image
· apply H'.continuousWithinAt.mono inter_subset_left
rw [mem_closure_iff_nhdsWithin_neBot]
exact I.mono (nhdsWithin_mono _ diff_subset)
