A priori estimates for maps approximating linear maps

An estimate controlling a vector by its image under a continuous linear map and an auxiliary additive map persists under a nonlinear approximation, with a loss proportional to the approximation constant. ApproximatesLinearOn.one_sub_mul_norm_sub_le records this absorption estimate. Taking the auxiliary map to be a projection onto the kernel gives the nonlinear form of the Peetre estimate used in local properness arguments.

Mathlib's local surjectivity and injectivity theorems also locate a unique zero of a map approximating a linear equivalence on a closed ball: ApproximatesLinearOn.exists_eq_zero_of_two_mul_norm_le.

A map on a convex set whose derivative stays close to a linear map A with a left inverse P is injective there, with injective derivative: P of the map approximates the identity (Convex.injOn_and_injective_of_norm_hasFDerivAt_sub_le).

If the derivative of a function g is approximated by a bilinear map L near x, a critical point y of g near x has a value within (‖L‖ + κ) * (2 * ρ) * ρ of that at x (ApproximatesLinearOn.norm_sub_le_of_fderiv_eq_zero).

theorem ApproximatesLinearOn.one_sub_mul_norm_sub_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {s : Set E} {ε : NNReal} (hf : ApproximatesLinearOn f f' s ε) {G : Type u_4} {𝓕 : Type u_5} [SeminormedAddGroup G] [FunLike 𝓕 E G] [AddMonoidHomClass 𝓕 E G] {P : 𝓕} {C : ℝ} (hC : 0 ≤ C) (hest : ∀ z ∈ s - s, ‖z‖ ≤ C * ‖f' z‖ + ‖P z‖) {x : E} (hx : x ∈ s) {y : E} (hy : y ∈ s) : (1 - C * ↑ε) * ‖x - y‖ ≤ C * ‖f x - f y‖ + ‖P x - P y‖

An a priori estimate for a linear map on s - s persists under a nonlinear approximation, with its left side scaled by 1 - C * ε. For C * ε < 1, this controls ‖x - y‖ by the images under f and an auxiliary additive map P.

Taking P to be a projection onto the kernel recovers the nonlinear Peetre estimate; see Wendl, Fredholm operators, Lemma 5.2, for the linear estimate.

theorem ApproximatesLinearOn.exists_eq_zero_of_two_mul_norm_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace E] {f : E → F} {f' : E ≃L[𝕜] F} {b : E} {r : ℝ} {c : NNReal} (hf : ApproximatesLinearOn f (↑f') (Metric.closedBall b r) c) {C : ℝ} (hC : 0 < C) (hf' : ‖↑f'.symm‖ ≤ C) (hc : 2 * C * ↑c ≤ 1) (hr : 2 * C * ‖f b‖ ≤ r) : ∃ a ∈ Metric.closedBall b (2 * C * ‖f b‖), f a = 0 ∧ ∀ z ∈ Metric.closedBall b r, f z = 0 → z = a

A map approximating a linear equivalence f' on a closed ball around b, with constant at most (2 * C)⁻¹ for a bound C on ‖f'⁻¹‖, has a zero within 2 * C * ‖f b‖ of b as soon as that radius fits in the ball, and this zero is the only zero of the map in the ball.

theorem ApproximatesLinearOn.norm_sub_le_of_fderiv_eq_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [IsRCLikeNormedField 𝕜] [NormedSpace ℝ E] {g : E → F} {L : E →L[𝕜] E →L[𝕜] F} {s : Set E} {κ : NNReal} (happrox : ApproximatesLinearOn (fderiv 𝕜 g) L s κ) {x y : E} {ρ : ℝ} (hg : ∀ w ∈ Metric.closedBall x ρ, DifferentiableAt 𝕜 g w) (hsub : Metric.closedBall x ρ ⊆ s) (hy : y ∈ Metric.closedBall x ρ) (hy0 : fderiv 𝕜 g y = 0) : ‖g y - g x‖ ≤ (‖L‖ + ↑κ) * (2 * ρ) * ρ

If fderiv 𝕜 g is κ-approximated by L on a set containing the closed ball of radius ρ about x, g is differentiable on that ball, and g has a critical point y in the ball, then g changes by at most (‖L‖ + κ) * (2 * ρ) * ρ between x and y.

theorem Convex.injOn_and_injective_of_norm_hasFDerivAt_sub_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {S : Set E} (hS : Convex ℝ S) {h : E → F} {h' : E → E →L[ℝ] F} {A : E →L[ℝ] F} {P : F →L[ℝ] E} (hPA : Function.LeftInverse ⇑P ⇑A) (hh : ∀ u ∈ S, HasFDerivAt h (h' u) u) (hh' : ∀ u ∈ S, ‖P‖ * ‖h' u - A‖ ≤ 1 / 2) : Set.InjOn h S ∧ ∀ u ∈ S, Function.Injective ⇑(h' u)

A map whose derivative is close to an injective linear map is injective on a convex set. If P is a left inverse of A and the derivative of h stays within 1 / (2 ‖P‖) of A on a convex set S, then h is injective on S, and its derivative is injective there.