English
If f approximates a linear map on s with a nonlinear right inverse, and either E is trivial or c is strictly smaller than the inverse of the right inverse norm, then f|_s is antilipschitz with constant (N^{-1}-c)^{-1}.
Русский
Если f аппроксимирует линейное отображение на s с нелинейным правым обратным и либо пространство тривиально, либо c меньше чем обратная норма этого обратного, то ограничение f на s является антилипшицевым с константой (N^{-1}-c)^{-1}.
LaTeX
$$$hf: ApproximatesLinearOn(f,f',s,c) \land (f'.NonlinearRightInverse)\Rightarrow \text{antilipschitz}_{(N^{-1}-c)^{-1}}(f|_s).$$$
Lean4
protected theorem antilipschitz (hf : ApproximatesLinearOn f (f' : E →L[𝕜] F) s c) (hc : Subsingleton E ∨ c < N⁻¹) :
AntilipschitzWith (N⁻¹ - c)⁻¹ (s.restrict f) :=
by
rcases hc with hE | hc
· exact AntilipschitzWith.of_subsingleton
convert (f'.antilipschitz.restrict s).add_lipschitzWith hf.lipschitz_sub hc
simp [restrict]
