English
The inverse of f restricted to s is approximated linearly by f'^{-1} on f(s) with a specific constant depending on N and c.
Русский
Обратная функция к f, ограниченная на s, аппроксимируется линейно посредством f'^{-1} на f(s) с константой, зависящей от N и c.
LaTeX
$$$\text{ApproximatesLinearOn} \left( hf.toPartialEquiv hc \right)^{-1} (f'.symm) (f'' s) \text{ with } N * (N^{-1} - c)^{-1} * c$$$
Lean4
/-- The inverse function is approximated linearly on `f '' s` by `f'.symm`. -/
theorem to_inv (hf : ApproximatesLinearOn f (f' : E →L[𝕜] F) s c) (hc : Subsingleton E ∨ c < N⁻¹) :
ApproximatesLinearOn (hf.toPartialEquiv hc).symm (f'.symm : F →L[𝕜] E) (f '' s) (N * (N⁻¹ - c)⁻¹ * c) :=
fun x hx y hy ↦ by
set A := hf.toPartialEquiv hc
have Af : ∀ z, A z = f z := fun z => rfl
rcases (mem_image _ _ _).1 hx with ⟨x', x's, rfl⟩
rcases (mem_image _ _ _).1 hy with ⟨y', y's, rfl⟩
rw [← Af x', ← Af y', A.left_inv x's, A.left_inv y's]
calc
‖x' - y' - f'.symm (A x' - A y')‖ ≤ N * ‖f' (x' - y' - f'.symm (A x' - A y'))‖ :=
(f' : E →L[𝕜] F).bound_of_antilipschitz f'.antilipschitz _
_ = N * ‖A y' - A x' - f' (y' - x')‖ := by
congr 2
simp only [ContinuousLinearEquiv.apply_symm_apply, ContinuousLinearEquiv.map_sub]
abel
_ ≤ N * (c * ‖y' - x'‖) := (mul_le_mul_of_nonneg_left (hf _ y's _ x's) (NNReal.coe_nonneg _))
_ ≤ N * (c * (((N⁻¹ - c)⁻¹ : ℝ≥0) * ‖A y' - A x'‖)) :=
by
gcongr
rw [← dist_eq_norm, ← dist_eq_norm]
exact (hf.antilipschitz hc).le_mul_dist ⟨y', y's⟩ ⟨x', x's⟩
_ = (N * (N⁻¹ - c)⁻¹ * c : ℝ≥0) * ‖A x' - A y'‖ := by simp only [norm_sub_rev, NNReal.coe_mul]; ring
