chore(analysis/normed_space/banach): move more to the continuous_linear_map NS (#11263)

## Rename

* `open_mapping` → `continuous_linear_map.is_open_map`;
* `open_mapping_affine` → `affine_map.is_open_map`;

### New lemmas

* `continuous_linear_map.quotient_map`,
* `continuous_linear_map.interior_preimage`,
* `continuous_linear_map.closure_preimage`,
* `continuous_linear_map.frontier_preimage`.

Author: urkud

docs/overview.yaml

@@ -248,7 +248,7 @@ Analysis:
     finite dimensional normed spaces over complete normed fields are complete: 'submodule.complete_of_finite_dimensional'
     Heine-Borel theorem (finite dimensional normed spaces are proper): 'finite_dimensional.proper'
     norm of a continuous linear map: 'linear_map.mk_continuous'
-    Banach open mapping theorem: 'open_mapping'
+    Banach open mapping theorem: 'continuous_linear_map.is_open_map'
     absolutely convergent series in Banach spaces: 'summable_of_summable_norm'
     Hahn-Banach theorem: 'exists_extension_norm_eq'
     dual of a normed space: 'normed_space.dual'

docs/undergrad.yaml

@@ -413,7 +413,7 @@ Topology:
   Normed vector spaces on $\R$ and $\C$:
     topology on a normed vector space: 'semi_normed_space.has_bounded_smul'
     equivalent norms: ''
-    Banach open mapping theorem: 'open_mapping'
+    Banach open mapping theorem: 'continuous_linear_map.is_open_map'
     equivalence of norms in finite dimension: 'linear_equiv.to_continuous_linear_equiv'
     norms $\lVert\cdot\rVert_p$ on $\R^n$ and $\C^n$: 'pi_Lp.normed_space'
     absolutely convergent series in Banach spaces: 'summable_of_summable_norm'

src/analysis/normed_space/add_torsor_bases.lean

@@ -32,13 +32,13 @@ variables (b : affine_basis ι 𝕜 P)
 
 @[continuity]
 lemma continuous_barycentric_coord (i : ι) : continuous (b.coord i) :=
-affine_map.continuous_of_finite_dimensional _
+(b.coord i).continuous_of_finite_dimensional
 
 local attribute [instance] finite_dimensional.complete
 
 lemma is_open_map_barycentric_coord [nontrivial ι] (i : ι) :
   is_open_map (b.coord i) :=
-open_mapping_affine (continuous_barycentric_coord b i) (b.surjective_coord i)
+(b.coord i).is_open_map (continuous_barycentric_coord b i) (b.surjective_coord i)
 
 end barycentric
 

src/analysis/normed_space/banach.lean

@@ -64,6 +64,7 @@ noncomputable instance (f : E ≃L[𝕜] F) :
 
 variable [complete_space F]
 
+namespace continuous_linear_map
 /--
 First step of the proof of the Banach open mapping theorem (using completeness of `F`):
 by Baire's theorem, there exists a ball in `E` whose image closure has nonempty interior.
@@ -194,14 +195,14 @@ begin
     ... = 2 * C * ∥y∥ : by rw [tsum_geometric_two, mul_assoc]
     ... ≤ 2 * C * ∥y∥ + ∥y∥ : le_add_of_nonneg_right (norm_nonneg y)
     ... = (2 * C + 1) * ∥y∥ : by ring,
-  have fsumeq : ∀n:ℕ, f (∑ i in range n, u i) = y - (h^[n]) y,
+  have fsumeq : ∀n:ℕ, f (∑ i in finset.range n, u i) = y - (h^[n]) y,
   { assume n,
     induction n with n IH,
     { simp [f.map_zero] },
     { rw [sum_range_succ, f.map_add, IH, iterate_succ', sub_add] } },
-  have : tendsto (λn, ∑ i in range n, u i) at_top (𝓝 x) :=
+  have : tendsto (λn, ∑ i in finset.range n, u i) at_top (𝓝 x) :=
     su.has_sum.tendsto_sum_nat,
-  have L₁ : tendsto (λn, f (∑ i in range n, u i)) at_top (𝓝 (f x)) :=
+  have L₁ : tendsto (λn, f (∑ i in finset.range n, u i)) at_top (𝓝 (f x)) :=
     (f.continuous.tendsto _).comp this,
   simp only [fsumeq] at L₁,
   have L₂ : tendsto (λn, y - (h^[n]) y) at_top (𝓝 (y - 0)),
@@ -218,7 +219,7 @@ end
 
 /-- The Banach open mapping theorem: a surjective bounded linear map between Banach spaces is
 open. -/
-theorem open_mapping (surj : surjective f) : is_open_map f :=
+protected theorem is_open_map (surj : surjective f) : is_open_map f :=
 begin
   assume s hs,
   rcases exists_preimage_norm_le f surj with ⟨C, Cpos, hC⟩,
@@ -240,20 +241,30 @@ begin
   exact set.mem_image_of_mem _ (hε this)
 end
 
-lemma open_mapping_affine {P Q : Type*}
+protected theorem quotient_map (surj : surjective f) : quotient_map f :=
+(f.is_open_map surj).to_quotient_map f.continuous surj
+
+lemma _root_.affine_map.is_open_map {P Q : Type*}
   [metric_space P] [normed_add_torsor E P] [metric_space Q] [normed_add_torsor F Q]
-  {f : P →ᵃ[𝕜] Q} (hf : continuous f) (surj : surjective f) :
+  (f : P →ᵃ[𝕜] Q) (hf : continuous f) (surj : surjective f) :
   is_open_map f :=
-begin
-  rw ← affine_map.is_open_map_linear_iff,
-  exact open_mapping
-    { cont := affine_map.continuous_linear_iff.mpr hf, .. f.linear }
-    (f.surjective_iff_linear_surjective.mpr surj),
-end
+affine_map.is_open_map_linear_iff.mp $ continuous_linear_map.is_open_map
+  { cont := affine_map.continuous_linear_iff.mpr hf, .. f.linear }
+  (f.surjective_iff_linear_surjective.mpr surj)
 
 /-! ### Applications of the Banach open mapping theorem -/
 
-namespace continuous_linear_map
+lemma interior_preimage (hsurj : surjective f) (s : set F) :
+  interior (f ⁻¹' s) = f ⁻¹' (interior s) :=
+((f.is_open_map hsurj).preimage_interior_eq_interior_preimage f.continuous s).symm
+
+lemma closure_preimage (hsurj : surjective f) (s : set F) :
+  closure (f ⁻¹' s) = f ⁻¹' (closure s) :=
+((f.is_open_map hsurj).preimage_closure_eq_closure_preimage f.continuous s).symm
+
+lemma frontier_preimage (hsurj : surjective f) (s : set F) :
+  frontier (f ⁻¹' s) = f ⁻¹' (frontier s) :=
+((f.is_open_map hsurj).preimage_frontier_eq_frontier_preimage f.continuous s).symm
 
 lemma exists_nonlinear_right_inverse_of_surjective (f : E →L[𝕜] F) (hsurj : f.range = ⊤) :
   ∃ (fsymm : nonlinear_right_inverse f), 0 < fsymm.nnnorm :=
@@ -285,6 +296,8 @@ end continuous_linear_map
 
 namespace linear_equiv
 
+variables [complete_space E]
+
 /-- If a bounded linear map is a bijection, then its inverse is also a bounded linear map. -/
 @[continuity]
 theorem continuous_symm (e : E ≃ₗ[𝕜] F) (h : continuous e) :
@@ -294,7 +307,7 @@ begin
   intros s hs,
   rw [← e.image_eq_preimage],
   rw [← e.coe_coe] at h ⊢,
-  exact open_mapping ⟨↑e, h⟩ e.surjective s hs
+  exact continuous_linear_map.is_open_map ⟨↑e, h⟩ e.surjective s hs
 end
 
 /-- Associating to a linear equivalence between Banach spaces a continuous linear equivalence when
@@ -317,7 +330,9 @@ end linear_equiv
 
 namespace continuous_linear_equiv
 
-/-- Convert a bijective continuous linear map `f : E →L[𝕜] F` between two Banach spaces
+variables [complete_space E]
+
+/-- Convert a bijective continuous linear map `f : E →L[𝕜] F` from a Banach space to a normed space
 to a continuous linear equivalence. -/
 noncomputable def of_bijective (f : E →L[𝕜] F) (hinj : f.ker = ⊥) (hsurj : f.range = ⊤) :
   E ≃L[𝕜] F :=
@@ -344,6 +359,8 @@ end continuous_linear_equiv
 
 namespace continuous_linear_map
 
+variables [complete_space E]
+
 /-- Intermediate definition used to show
 `continuous_linear_map.closed_complemented_range_of_is_compl_of_ker_eq_bot`.
 
@@ -375,7 +392,7 @@ lemma closed_complemented_range_of_is_compl_of_ker_eq_bot (f : E →L[𝕜] F) (
   (h : is_compl f.range G) (hG : is_closed (G : set F)) (hker : f.ker = ⊥) :
   is_closed (f.range : set F) :=
 begin
-  haveI : complete_space G := complete_space_coe_iff_is_complete.2 hG.is_complete,
+  haveI : complete_space G := hG.complete_space_coe,
   let g := coprod_subtypeL_equiv_of_is_compl f h hker,
   rw congr_arg coe (range_eq_map_coprod_subtypeL_equiv_of_is_compl f h hker ),
   apply g.to_homeomorph.is_closed_image.2,