English
If f is approximated on the whole space by a linear surrogate with univ domain and with a bound c, and either E is subsingleton or c < 1/N, then f is surjective.
Русский
Если функция f аппроксимируется на всей пространстве аппроксимацией линейного отображения с доменом равным всему пространству и константой c, и либо E одноэлементно, либо c < 1/N, то f отображает на всю целевую область.
LaTeX
$$$\text{ApproximatesLinearOn } f (f' : E \to L[𝕜] F)\ Set.univ\ c \;\to\ (Subsingleton E \;\lor\; c < N^{-1}) \;\to\; \text{Surjective } f$$$
Lean4
protected theorem surjective [CompleteSpace E] (hf : ApproximatesLinearOn f (f' : E →L[𝕜] F) univ c)
(hc : Subsingleton E ∨ c < N⁻¹) : Surjective f :=
by
rcases hc with hE | hc
· haveI : Subsingleton F := (Equiv.subsingleton_congr f'.toEquiv).1 hE
exact surjective_to_subsingleton _
· apply forall_of_forall_mem_closedBall (fun y : F => ∃ a, f a = y) (f 0) _
have hc' : (0 : ℝ) < N⁻¹ - c := by rw [sub_pos]; exact hc
let p : ℝ → Prop := fun R => closedBall (f 0) R ⊆ Set.range f
have hp : ∀ᶠ r : ℝ in atTop, p ((N⁻¹ - c) * r) :=
by
have hr : ∀ᶠ r : ℝ in atTop, 0 ≤ r := eventually_ge_atTop 0
refine hr.mono fun r hr => Subset.trans ?_ (image_subset_range f (closedBall 0 r))
refine hf.surjOn_closedBall_of_nonlinearRightInverse f'.toNonlinearRightInverse hr ?_
exact subset_univ _
refine ((tendsto_id.const_mul_atTop hc').frequently hp.frequently).mono ?_
exact fun R h y hy => h hy
