English
If f approximates a nonlinear right inverse with a contraction-like bound on s and ε-ball around b lies in s, then the image of f contains a closed ball around f(b) with an explicit radius.
Русский
Если функция f аппроксимирует нелинейное правое обратное с согласованным пределом на s и шар вокруг b вложен в s, тогда изображение f содержит замкнутый шар вокруг f(b) с явным радиусом.
LaTeX
$$$\text{SurjOn}(f,\overline{B}(b,\varepsilon),\overline{B}(f(b),((\|f'\|)^{-1}-c)\varepsilon))$$$
Lean4
/-- If a function is linearly approximated by a continuous linear map with a (possibly nonlinear)
right inverse, then it is locally onto: a ball of an explicit radius is included in the image
of the map. -/
theorem surjOn_closedBall_of_nonlinearRightInverse (hf : ApproximatesLinearOn f f' s c)
(f'symm : f'.NonlinearRightInverse) {ε : ℝ} {b : E} (ε0 : 0 ≤ ε) (hε : closedBall b ε ⊆ s) :
SurjOn f (closedBall b ε) (closedBall (f b) (((f'symm.nnnorm : ℝ)⁻¹ - c) * ε)) :=
by
intro y hy
rcases le_or_gt (f'symm.nnnorm : ℝ)⁻¹ c with hc | hc
· refine ⟨b, by simp [ε0], ?_⟩
have : dist y (f b) ≤ 0 := (mem_closedBall.1 hy).trans (mul_nonpos_of_nonpos_of_nonneg (by linarith) ε0)
simp only [dist_le_zero] at this
rw [this]
have If' : (0 : ℝ) < f'symm.nnnorm := by rw [← inv_pos]; exact (NNReal.coe_nonneg _).trans_lt hc
have Icf' : (c : ℝ) * f'symm.nnnorm < 1 := by rwa [inv_eq_one_div, lt_div_iff₀ If'] at hc
have Jcf' : (1 : ℝ) - c * f'symm.nnnorm ≠ 0 := by apply ne_of_gt;
linarith
/- We have to show that `y` can be written as `f x` for some `x ∈ closedBall b ε`.
The idea of the proof is to apply the Banach contraction principle to the map
`g : x ↦ x + f'symm (y - f x)`, as a fixed point of this map satisfies `f x = y`.
When `f'symm` is a genuine linear inverse, `g` is a contracting map. In our case, since `f'symm`
is nonlinear, this map is not contracting (it is not even continuous), but still the proof of
the contraction theorem holds: `uₙ = gⁿ b` is a Cauchy sequence, converging exponentially fast
to the desired point `x`. Instead of appealing to general results, we check this by hand.
The main point is that `f (u n)` becomes exponentially close to `y`, and therefore
`dist (u (n+1)) (u n)` becomes exponentally small, making it possible to get an inductive
bound on `dist (u n) b`, from which one checks that `u n` stays in the ball on which one has a
control. Therefore, the bound can be checked at the next step, and so on inductively.
-/
set g := fun x => x + f'symm (y - f x) with hg
set u := fun n : ℕ => g^[n] b with hu
have usucc : ∀ n, u (n + 1) = g (u n) := by
simp [hu, ← iterate_succ_apply' g _ b]
-- First bound: if `f z` is close to `y`, then `g z` is close to `z` (i.e., almost a fixed point).
have A : ∀ z, dist (g z) z ≤ f'symm.nnnorm * dist (f z) y :=
by
intro z
rw [dist_eq_norm, hg, add_sub_cancel_left, dist_eq_norm']
exact
f'symm.bound
_
-- Second bound: if `z` and `g z` are in the set with good control, then `f (g z)` becomes closer
-- to `y` than `f z` was (this uses the linear approximation property, and is the reason for the
-- choice of the formula for `g`).
have B : ∀ z ∈ closedBall b ε, g z ∈ closedBall b ε → dist (f (g z)) y ≤ c * f'symm.nnnorm * dist (f z) y :=
by
intro z hz hgz
set v := f'symm (y - f z)
calc
dist (f (g z)) y = ‖f (z + v) - y‖ := by rw [dist_eq_norm]
_ = ‖f (z + v) - f z - f' v + f' v - (y - f z)‖ := by congr 1; abel
_ = ‖f (z + v) - f z - f' (z + v - z)‖ := by
simp only [v, ContinuousLinearMap.NonlinearRightInverse.right_inv, add_sub_cancel_left, sub_add_cancel]
_ ≤ c * ‖z + v - z‖ := (hf _ (hε hgz) _ (hε hz))
_ ≤ c * (f'symm.nnnorm * dist (f z) y) := by
gcongr
simpa [dist_eq_norm'] using f'symm.bound (y - f z)
_ = c * f'symm.nnnorm * dist (f z) y := by
ring
-- Third bound: a complicated bound on `dist w b` (that will show up in the induction) is enough
-- to check that `w` is in the ball on which one has controls. Will be used to check that `u n`
-- belongs to this ball for all `n`.
have C :
∀ (n : ℕ) (w : E),
dist w b ≤ f'symm.nnnorm * (1 - ((c : ℝ) * f'symm.nnnorm) ^ n) / (1 - c * f'symm.nnnorm) * dist (f b) y →
w ∈ closedBall b ε :=
fun n w hw ↦ by
apply hw.trans
rw [div_mul_eq_mul_div, div_le_iff₀]; swap; · linarith
calc
(f'symm.nnnorm : ℝ) * (1 - ((c : ℝ) * f'symm.nnnorm) ^ n) * dist (f b) y =
f'symm.nnnorm * dist (f b) y * (1 - ((c : ℝ) * f'symm.nnnorm) ^ n) :=
by ring
_ ≤ f'symm.nnnorm * dist (f b) y * 1 := by
gcongr
rw [sub_le_self_iff]
positivity
_ ≤ f'symm.nnnorm * (((f'symm.nnnorm : ℝ)⁻¹ - c) * ε) :=
by
rw [mul_one]
gcongr
exact mem_closedBall'.1 hy
_ = ε * (1 - c * f'symm.nnnorm) := by
field_simp
/- Main inductive control: `f (u n)` becomes exponentially close to `y`, and therefore
`dist (u (n+1)) (u n)` becomes exponentally small, making it possible to get an inductive
bound on `dist (u n) b`, from which one checks that `u n` remains in the ball on which we
have estimates. -/
have D :
∀ n : ℕ,
dist (f (u n)) y ≤ ((c : ℝ) * f'symm.nnnorm) ^ n * dist (f b) y ∧
dist (u n) b ≤
f'symm.nnnorm * (1 - ((c : ℝ) * f'symm.nnnorm) ^ n) / (1 - (c : ℝ) * f'symm.nnnorm) * dist (f b) y :=
fun n ↦
by
induction n with
| zero => simp [hu, le_refl]
| succ n IH => ?_
rw [usucc]
have Ign :
dist (g (u n)) b ≤
f'symm.nnnorm * (1 - ((c : ℝ) * f'symm.nnnorm) ^ n.succ) / (1 - c * f'symm.nnnorm) * dist (f b) y :=
calc
dist (g (u n)) b ≤ dist (g (u n)) (u n) + dist (u n) b := dist_triangle _ _ _
_ ≤ f'symm.nnnorm * dist (f (u n)) y + dist (u n) b := (add_le_add (A _) le_rfl)
_ ≤
f'symm.nnnorm * (((c : ℝ) * f'symm.nnnorm) ^ n * dist (f b) y) +
f'symm.nnnorm * (1 - ((c : ℝ) * f'symm.nnnorm) ^ n) / (1 - c * f'symm.nnnorm) * dist (f b) y :=
by
gcongr
· exact IH.1
· exact IH.2
_ = f'symm.nnnorm * (1 - ((c : ℝ) * f'symm.nnnorm) ^ n.succ) / (1 - (c : ℝ) * f'symm.nnnorm) * dist (f b) y :=
by
replace Jcf' : (1 : ℝ) - f'symm.nnnorm * c ≠ 0 := by convert Jcf' using 1; ring
simp [field, pow_succ, -mul_eq_mul_left_iff]
ring
refine ⟨?_, Ign⟩
calc
dist (f (g (u n))) y ≤ c * f'symm.nnnorm * dist (f (u n)) y := B _ (C n _ IH.2) (C n.succ _ Ign)
_ ≤ (c : ℝ) * f'symm.nnnorm * (((c : ℝ) * f'symm.nnnorm) ^ n * dist (f b) y) :=
by
gcongr
apply IH.1
_ = ((c : ℝ) * f'symm.nnnorm) ^ n.succ * dist (f b) y := by simp only [pow_succ'];
ring
-- Deduce from the inductive bound that `uₙ` is a Cauchy sequence, therefore converging.
have : CauchySeq u :=
by
refine cauchySeq_of_le_geometric _ (↑f'symm.nnnorm * dist (f b) y) Icf' fun n ↦ ?_
calc
dist (u n) (u (n + 1)) = dist (g (u n)) (u n) := by rw [usucc, dist_comm]
_ ≤ f'symm.nnnorm * dist (f (u n)) y := (A _)
_ ≤ f'symm.nnnorm * (((c : ℝ) * f'symm.nnnorm) ^ n * dist (f b) y) :=
by
gcongr
exact (D n).1
_ = f'symm.nnnorm * dist (f b) y * ((c : ℝ) * f'symm.nnnorm) ^ n := by ring
obtain ⟨x, hx⟩ : ∃ x, Tendsto u atTop (𝓝 x) := cauchySeq_tendsto_of_complete this
have xmem : x ∈ closedBall b ε := isClosed_closedBall.mem_of_tendsto hx (Eventually.of_forall fun n => C n _ (D n).2)
refine
⟨x, xmem, ?_⟩
-- It remains to check that `f x = y`. This follows from continuity of `f` on `closedBall b ε`
-- and from the fact that `f uₙ` is converging to `y` by construction.
have hx' : Tendsto u atTop (𝓝[closedBall b ε] x) :=
by
simp only [nhdsWithin, tendsto_inf, hx, true_and, tendsto_principal]
exact Eventually.of_forall fun n => C n _ (D n).2
have T1 : Tendsto (f ∘ u) atTop (𝓝 (f x)) := (hf.continuousOn.mono hε x xmem).tendsto.comp hx'
have T2 : Tendsto (f ∘ u) atTop (𝓝 y) := by
rw [tendsto_iff_dist_tendsto_zero]
refine squeeze_zero (fun _ => dist_nonneg) (fun n => (D n).1) ?_
simpa using (tendsto_pow_atTop_nhds_zero_of_lt_one (by positivity) Icf').mul tendsto_const_nhds
exact tendsto_nhds_unique T1 T2
