feat(analysis/calculus/inverse): a map which approximates a linear ma…

…p on a set admits a nice global extension (#11568)

And several other results on maps that are well approximated by linear maps on some subset of the space (not necessarily open).

src/analysis/calculus/inverse.lean

@@ -108,6 +108,10 @@ on a specific set. -/
 def approximates_linear_on (f : E → F) (f' : E →L[𝕜] F) (s : set E) (c : ℝ≥0) : Prop :=
 ∀ (x ∈ s) (y ∈ s), ∥f x - f y - f' (x - y)∥ ≤ c * ∥x - y∥
 
+@[simp] lemma approximates_linear_on_empty (f : E → F) (f' : E →L[𝕜] F) (c : ℝ≥0) :
+  approximates_linear_on f f' ∅ c :=
+by simp [approximates_linear_on]
+
 namespace approximates_linear_on
 
 variables [cs : complete_space E] {f : E → F}
@@ -127,6 +131,18 @@ theorem mono_set (hst : s ⊆ t) (hf : approximates_linear_on f f' t c) :
   approximates_linear_on f f' s c :=
 λ x hx y hy, hf x (hst hx) y (hst hy)
 
+lemma approximates_linear_on_iff_lipschitz_on_with
+  {f : E → F} {f' : E →L[𝕜] F} {s : set E} {c : ℝ≥0} :
+  approximates_linear_on f f' s c ↔ lipschitz_on_with c (f - f') s :=
+begin
+  have : ∀ x y, f x - f y - f' (x - y) = (f - f') x - (f - f') y,
+  { assume x y, simp only [map_sub, pi.sub_apply], abel },
+  simp only [this, lipschitz_on_with_iff_norm_sub_le, approximates_linear_on],
+end
+
+alias approximates_linear_on_iff_lipschitz_on_with ↔
+  approximates_linear_on.lipschitz_on_with lipschitz_on_with.approximates_linear_on
+
 lemma lipschitz_sub (hf : approximates_linear_on f f' s c) :
   lipschitz_with c (λ x : s, f x - f' x) :=
 begin
@@ -298,7 +314,7 @@ begin
   exact tendsto_nhds_unique T1 T2,
 end
 
-lemma open_image (hf : approximates_linear_on f f' s c)  (f'symm : f'.nonlinear_right_inverse)
+lemma open_image (hf : approximates_linear_on f f' s c) (f'symm : f'.nonlinear_right_inverse)
   (hs : is_open s) (hc : subsingleton F ∨ c < f'symm.nnnorm⁻¹) : is_open (f '' s) :=
 begin
   cases hc with hE hc, { resetI, apply is_open_discrete },
@@ -363,6 +379,25 @@ protected lemma inj_on (hf : approximates_linear_on f (f' : E →L[𝕜] F) s c)
   inj_on f s :=
 inj_on_iff_injective.2 $ hf.injective hc
 
+protected lemma surjective [complete_space E]
+  (hf : approximates_linear_on f (f' : E →L[𝕜] F) univ c) (hc : subsingleton E ∨ c < N⁻¹) :
+  surjective f :=
+begin
+  cases hc with hE hc,
+  { haveI : subsingleton F := (equiv.subsingleton_congr f'.to_linear_equiv.to_equiv).1 hE,
+    exact surjective_to_subsingleton _ },
+  { apply forall_of_forall_mem_closed_ball (λ (y : F), ∃ a, f a = y) (f 0) _,
+    have hc' : (0 : ℝ) < N⁻¹ - c, by { rw sub_pos, exact hc },
+    let p : ℝ → Prop := λ R, closed_ball (f 0) R ⊆ set.range f,
+    have hp : ∀ᶠ (r:ℝ) in at_top, p ((N⁻¹ - c) * r),
+    { have hr : ∀ᶠ (r:ℝ) in at_top, 0 ≤ r := eventually_ge_at_top 0,
+      refine hr.mono (λ r hr, subset.trans _ (image_subset_range f (closed_ball 0 r))),
+      refine hf.surj_on_closed_ball_of_nonlinear_right_inverse f'.to_nonlinear_right_inverse hr _,
+      exact subset_univ _ },
+    refine ((tendsto_id.const_mul_at_top hc').frequently hp.frequently).mono _,
+    exact λ R h y hy, h hy },
+end
+
 /-- A map approximating a linear equivalence on a set defines a local equivalence on this set.
 Should not be used outside of this file, because it is superseded by `to_local_homeomorph` below.
 
@@ -381,6 +416,39 @@ begin
   exact (λ x hx, (hf.to_local_equiv hc).map_target hx)
 end
 
+/-- The inverse function is approximated linearly on `f '' s` by `f'.symm`. -/
+lemma to_inv (hf : approximates_linear_on f (f' : E →L[𝕜] F) s c)
+  (hc : subsingleton E ∨ c < N⁻¹) :
+  approximates_linear_on (hf.to_local_equiv hc).symm (f'.symm : F →L[𝕜] E) (f '' s)
+    (N * (N⁻¹ - c)⁻¹ * c) :=
+begin
+  assume x hx y hy,
+  set A := hf.to_local_equiv hc with hA,
+  have Af : ∀ z, A z = f z := λ 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')∥ :
+    begin
+      congr' 2,
+      simp only [continuous_linear_equiv.apply_symm_apply, continuous_linear_equiv.map_sub],
+      abel,
+    end
+  ... ≤ 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'∥)) :
+    begin
+      apply_rules [mul_le_mul_of_nonneg_left, nnreal.coe_nonneg],
+      rw [← dist_eq_norm, ← dist_eq_norm],
+      exact (hf.antilipschitz hc).le_mul_dist ⟨y', y's⟩ ⟨x', x's⟩,
+    end
+  ... = (N * (N⁻¹ - c)⁻¹ * c : ℝ≥0) * ∥A x' - A y'∥ :
+    by { simp only [norm_sub_rev, nonneg.coe_mul], ring }
+end
+
 include cs
 
 section
@@ -397,6 +465,46 @@ def to_local_homeomorph (hf : approximates_linear_on f (f' : E →L[𝕜] F) s c
   continuous_to_fun := hf.continuous_on,
   continuous_inv_fun := hf.inverse_continuous_on hc }
 
+/-- A function `f` that approximates a linear equivalence on the whole space is a homeomorphism. -/
+def to_homeomorph (hf : approximates_linear_on f (f' : E →L[𝕜] F) univ c)
+  (hc : subsingleton E ∨ c < N⁻¹) :
+  E ≃ₜ F :=
+begin
+  refine (hf.to_local_homeomorph _ _ hc is_open_univ).to_homeomorph_of_source_eq_univ_target_eq_univ
+    rfl _,
+  change f '' univ = univ,
+  rw [image_univ, range_iff_surjective],
+  exact hf.surjective hc,
+end
+
+omit cs
+
+/-- In a real vector space, a function `f` that approximates a linear equivalence on a subset `s`
+can be extended to a homeomorphism of the whole space. -/
+lemma exists_homeomorph_extension {E : Type*} [normed_group E] [normed_space ℝ E]
+  {F : Type*} [normed_group F] [normed_space ℝ F] [finite_dimensional ℝ F]
+  {s : set E} {f : E → F} {f' : E ≃L[ℝ] F} {c : ℝ≥0}
+  (hf : approximates_linear_on f (f' : E →L[ℝ] F) s c)
+  (hc : subsingleton E ∨ lipschitz_extension_constant F * c < (∥(f'.symm : F →L[ℝ] E)∥₊)⁻¹) :
+  ∃ g : E ≃ₜ F, eq_on f g s :=
+begin
+  -- the difference `f - f'` is Lipschitz on `s`. It can be extended to a Lipschitz function `u`
+  -- on the whole space, with a slightly worse Lipschitz constant. Then `f' + u` will be the
+  -- desired homeomorphism.
+  obtain ⟨u, hu, uf⟩ : ∃ (u : E → F), lipschitz_with (lipschitz_extension_constant F * c) u
+    ∧ eq_on (f - f') u s := hf.lipschitz_on_with.extend_finite_dimension,
+  let g : E → F := λ x, f' x + u x,
+  have fg : eq_on f g s := λ x hx, by simp_rw [g, ← uf hx, pi.sub_apply, add_sub_cancel'_right],
+  have hg : approximates_linear_on g (f' : E →L[ℝ] F) univ (lipschitz_extension_constant F * c),
+  { apply lipschitz_on_with.approximates_linear_on,
+    rw lipschitz_on_univ,
+    convert hu,
+    ext x,
+    simp only [add_sub_cancel', continuous_linear_equiv.coe_coe, pi.sub_apply] },
+  haveI : finite_dimensional ℝ E := f'.symm.to_linear_equiv.finite_dimensional,
+  exact ⟨hg.to_homeomorph g hc, fg⟩,
+end
+
 end
 
 @[simp] lemma to_local_homeomorph_coe (hf : approximates_linear_on f (f' : E →L[𝕜] F) s c)

src/analysis/normed_space/operator_norm.lean

@@ -278,6 +278,14 @@ le_antisymm (φ.op_norm_le_bound M_nonneg h_above)
 
 lemma op_norm_neg (f : E →SL[σ₁₂] F) : ∥-f∥ = ∥f∥ := by simp only [norm_def, neg_apply, norm_neg]
 
+theorem antilipschitz_of_bound (f : E →SL[σ₁₂] F) {K : ℝ≥0} (h : ∀ x, ∥x∥ ≤ K * ∥f x∥) :
+  antilipschitz_with K f :=
+linear_map.antilipschitz_of_bound _ h
+
+lemma bound_of_antilipschitz (f : E →SL[σ₁₂] F) {K : ℝ≥0} (h : antilipschitz_with K f) (x) :
+  ∥x∥ ≤ K * ∥f x∥ :=
+linear_map.bound_of_antilipschitz _ h x
+
 section
 
 variables [ring_hom_isometric σ₁₂] [ring_hom_isometric σ₂₃]

src/order/filter/at_top_bot.lean

@@ -38,6 +38,8 @@ def at_bot [preorder α] : filter α := ⨅ a, 𝓟 (Iic a)
 lemma mem_at_top [preorder α] (a : α) : {b : α | a ≤ b} ∈ @at_top α _ :=
 mem_infi_of_mem a $ subset.refl _
 
+lemma Ici_mem_at_top [preorder α] (a : α) : Ici a ∈ (at_top : filter α) := mem_at_top a
+
 lemma Ioi_mem_at_top [preorder α] [no_max_order α] (x : α) : Ioi x ∈ (at_top : filter α) :=
 let ⟨z, hz⟩ := exists_gt x in mem_of_superset (mem_at_top z) $ λ y h,  lt_of_lt_of_le hz h
 

src/topology/metric_space/basic.lean

@@ -496,6 +496,28 @@ ball_subset $ by rw sub_self_div_two; exact le_of_lt h
 theorem exists_ball_subset_ball (h : y ∈ ball x ε) : ∃ ε' > 0, ball y ε' ⊆ ball x ε :=
 ⟨_, sub_pos.2 h, ball_subset $ by rw sub_sub_self⟩
 
+/-- If a property holds for all points in closed balls of arbitrarily large radii, then it holds for
+all points. -/
+lemma forall_of_forall_mem_closed_ball (p : α → Prop) (x : α)
+  (H : ∃ᶠ (R : ℝ) in at_top, ∀ y ∈ closed_ball x R, p y) (y : α) :
+  p y :=
+begin
+  obtain ⟨R, hR, h⟩ : ∃ (R : ℝ) (H : dist y x ≤ R), ∀ (z : α), z ∈ closed_ball x R → p z :=
+    frequently_iff.1 H (Ici_mem_at_top (dist y x)),
+  exact h _ hR
+end
+
+/-- If a property holds for all points in balls of arbitrarily large radii, then it holds for all
+points. -/
+lemma forall_of_forall_mem_ball (p : α → Prop) (x : α)
+  (H : ∃ᶠ (R : ℝ) in at_top, ∀ y ∈ ball x R, p y) (y : α) :
+  p y :=
+begin
+  obtain ⟨R, hR, h⟩ : ∃ (R : ℝ) (H : dist y x < R), ∀ (z : α), z ∈ ball x R → p z :=
+    frequently_iff.1 H (Ioi_mem_at_top (dist y x)),
+  exact h _ hR
+end
+
 theorem uniformity_basis_dist :
   (𝓤 α).has_basis (λ ε : ℝ, 0 < ε) (λ ε, {p:α×α | dist p.1 p.2 < ε}) :=
 begin