refactor(analysis/calculus/tangent_cone): split a proof into parts (#…

…2013)

* refactor(analysis/calculus/tangent_cone): split a proof into parts

Prove `submodule.eq_top_of_nonempty_interior` and use it in the
proof of `unique_diff_on_convex`.

* Update src/analysis/normed_space/basic.lean

Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr>

* Fix a docstring.

* Update src/topology/algebra/module.lean

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

src/algebra/associated.lean

@@ -14,6 +14,10 @@ open lattice
 
 theorem is_unit.mk0 [division_ring α] (x : α) (hx : x ≠ 0) : is_unit x := is_unit_unit (units.mk0 x hx)
 
+theorem is_unit_iff_ne_zero [division_ring α] {x : α} :
+  is_unit x ↔ x ≠ 0 :=
+⟨λ ⟨u, hu⟩, hu.symm ▸ λ h : u.1 = 0, by simpa [h, zero_ne_one] using u.3, is_unit.mk0 x⟩
+
 @[simp] theorem is_unit_zero_iff [semiring α] : is_unit (0 : α) ↔ (0:α) = 1 :=
 ⟨λ ⟨⟨_, a, (a0 : 0 * a = 1), _⟩, rfl⟩, by rwa zero_mul at a0,
  λ h, begin

src/algebra/module.lean

@@ -314,6 +314,9 @@ lemma sum_mem {ι : Type w} [decidable_eq ι] {t : finset ι} {f : ι → β} :
   (∀c∈t, f c ∈ p) → t.sum f ∈ p :=
 finset.induction_on t (by simp [p.zero_mem]) (by simp [p.add_mem] {contextual := tt})
 
+lemma smul_mem_iff' (u : units α) : (u:α) • x ∈ p ↔ x ∈ p :=
+⟨λ h, by simpa only [smul_smul, u.inv_mul, one_smul] using p.smul_mem ↑u⁻¹ h, p.smul_mem u⟩
+
 instance : has_add p := ⟨λx y, ⟨x.1 + y.1, add_mem _ x.2 y.2⟩⟩
 instance : has_zero p := ⟨⟨0, zero_mem _⟩⟩
 instance : inhabited p := ⟨0⟩
@@ -416,8 +419,7 @@ include R
 set_option class.instance_max_depth 36
 
 theorem smul_mem_iff (r0 : r ≠ 0) : r • x ∈ p ↔ x ∈ p :=
-⟨λ h, by simpa [smul_smul, inv_mul_cancel r0] using p.smul_mem (r⁻¹) h,
- p.smul_mem r⟩
+p.smul_mem_iff' (units.mk0 r r0)
 
 end submodule
 

src/analysis/calculus/tangent_cone.lean

@@ -329,39 +329,15 @@ theorem unique_diff_on_convex {s : set G} (conv : convex s) (hs : (interior s).n
   unique_diff_on ℝ s :=
 begin
   assume x xs,
-  have A : ∀v, ∃a∈ tangent_cone_at ℝ s x, ∃b∈ tangent_cone_at ℝ s x, ∃δ>(0:ℝ), δ • v = b-a,
-  { assume v,
-    rcases hs with ⟨y, hy⟩,
-    have ys : y ∈ s := interior_subset hy,
-    have : ∃(δ : ℝ), 0<δ ∧ y + δ • v ∈ s,
-    { by_cases h : ∥v∥ = 0,
-      { exact ⟨1, zero_lt_one, by simp [norm_eq_zero.1 h, ys]⟩ },
-      { rcases mem_interior.1 hy with ⟨u, us, u_open, yu⟩,
-        rcases metric.is_open_iff.1 u_open y yu with ⟨ε, εpos, hε⟩,
-        let δ := (ε/2) / ∥v∥,
-        have δpos : 0 < δ := div_pos (half_pos εpos) (lt_of_le_of_ne (norm_nonneg _) (ne.symm h)),
-        have : y + δ • v ∈ s,
-        { apply us (hε _),
-          rw [metric.mem_ball, dist_eq_norm],
-          calc ∥(y + δ • v) - y ∥ = ∥δ • v∥ : by {congr' 1, abel }
-          ... = ∥δ∥ * ∥v∥ : norm_smul _ _
-          ... = δ * ∥v∥ : by simp only [norm, abs_of_nonneg (le_of_lt δpos)]
-          ... = ε /2 : div_mul_cancel _ h
-          ... < ε : half_lt_self εpos },
-        exact ⟨δ, δpos, this⟩ } },
-    rcases this with ⟨δ, δpos, hδ⟩,
-    refine ⟨y-x, _, (y + δ • v) - x, _, δ, δpos, by abel⟩,
-    exact mem_tangent_cone_of_segment_subset (conv.segment_subset xs ys),
-    exact mem_tangent_cone_of_segment_subset (conv.segment_subset xs hδ) },
-  have B : ∀v:G, v ∈ submodule.span ℝ (tangent_cone_at ℝ s x),
-  { assume v,
-    rcases A v with ⟨a, ha, b, hb, δ, hδ, h⟩,
-    have : v = δ⁻¹ • (b - a),
-      by { rw [← h, smul_smul, inv_mul_cancel, one_smul], exact (ne_of_gt hδ) },
-    rw this,
-    exact submodule.smul_mem _ _
-      (submodule.sub_mem _ (submodule.subset_span hb) (submodule.subset_span ha)) },
-  refine ⟨univ_subset_iff.1 (λv hv, subset_closure (B v)), subset_closure xs⟩
+  rcases hs with ⟨y, hy⟩,
+  suffices : y - x ∈ interior (tangent_cone_at ℝ s x),
+  { refine ⟨_, subset_closure xs⟩,
+    rw [submodule.eq_top_of_nonempty_interior _ ⟨y - x, interior_mono submodule.subset_span this⟩,
+      submodule.top_coe, closure_univ] },
+  rw [mem_interior_iff_mem_nhds] at hy ⊢,
+  apply mem_sets_of_superset ((is_open_map_add_right (-x)).image_mem_nhds hy),
+  rintros _ ⟨z, zs, rfl⟩,
+  exact mem_tangent_cone_of_segment_subset (conv.segment_subset xs zs)
 end
 
 /-- The real interval `[0, 1]` is a set of unique differentiability. -/

src/analysis/normed_space/basic.lean

@@ -493,6 +493,16 @@ let ⟨n, hle, hlt⟩ := exists_int_pow_near' hr hw in
 ⟨w^n, by { rw norm_fpow; exact fpow_pos_of_pos (lt_trans zero_lt_one hw) _},
 by rwa norm_fpow⟩
 
+lemma punctured_nhds_ne_bot {α : Type*} [nondiscrete_normed_field α] (x : α) :
+  nhds_within x (-{x}) ≠ ⊥ :=
+begin
+  rw [← mem_closure_iff_nhds_within_ne_bot, metric.mem_closure_iff],
+  rintros ε ε0,
+  rcases normed_field.exists_norm_lt α ε0 with ⟨b, hb0, hbε⟩,
+  refine ⟨x + b, mt (set.mem_singleton_iff.trans add_right_eq_self).1 $ norm_pos_iff.1 hb0, _⟩,
+  rwa [dist_comm, dist_eq_norm, add_sub_cancel'],
+end
+
 lemma tendsto_inv [normed_field α] {r : α} (r0 : r ≠ 0) : tendsto (λq, q⁻¹) (𝓝 r) (𝓝 r⁻¹) :=
 begin
   refine (nhds_basis_closed_ball.tendsto_iff nhds_basis_closed_ball).2 (λε εpos, _),
@@ -635,6 +645,16 @@ begin
             (tendsto_const_nhds.mul (tendsto_iff_norm_tendsto_zero.1 (continuous_snd.tendsto p))) }
 end
 
+/-- In a normed space over a nondiscrete normed field, only `⊤` submodule has a nonempty interior.
+See also `submodule.eq_top_of_nonempty_interior'` for a `topological_module` version.  -/
+lemma submodule.eq_top_of_nonempty_interior {α E : Type*} [nondiscrete_normed_field α] [normed_group E]
+  [normed_space α E] (s : submodule α E) (hs : (interior (s:set E)).nonempty) :
+  s = ⊤ :=
+begin
+  refine s.eq_top_of_nonempty_interior' _ hs,
+  simp only [is_unit_iff_ne_zero, @ne.def α, set.mem_singleton_iff.symm],
+  exact normed_field.punctured_nhds_ne_bot _
+end
 
 open normed_field
 

src/topology/algebra/module.lean

@@ -112,6 +112,27 @@ lemma is_open_map_smul_of_unit (a : units R) : is_open_map (λ (x : M), (a : R)
 lemma is_closed_map_smul_of_unit (a : units R) : is_closed_map (λ (x : M), (a : R) • x) :=
 (homeomorph.smul_of_unit a).is_closed_map
 
+/-- If `M` is a topological module over `R` and `0` is a limit of invertible elements of `R`, then
+`⊤` is the only submodule of `M` with a nonempty interior. See also
+`submodule.eq_top_of_nonempty_interior` for a `normed_space` version. -/
+lemma submodule.eq_top_of_nonempty_interior' [topological_add_monoid M]
+  (h : nhds_within (0:R) {x | is_unit x} ≠ ⊥)
+  (s : submodule R M) (hs : (interior (s:set M)).nonempty) :
+  s = ⊤ :=
+begin
+  rcases hs with ⟨y, hy⟩,
+  refine (submodule.eq_top_iff'.2 $ λ x, _),
+  rw [mem_interior_iff_mem_nhds] at hy,
+  have : tendsto (λ c:R, y + c • x) (nhds_within 0 {x | is_unit x}) (𝓝 (y + (0:R) • x)),
+    from tendsto_const_nhds.add ((tendsto_nhds_within_of_tendsto_nhds tendsto_id).smul
+      tendsto_const_nhds),
+  rw [zero_smul, add_zero] at this,
+  rcases nonempty_of_mem_sets h (inter_mem_sets (mem_map.1 (this hy)) self_mem_nhds_within)
+    with ⟨_, hu, u, rfl⟩,
+  have hy' : y ∈ ↑s := mem_of_nhds hy,
+  exact (s.smul_mem_iff' _).1 ((s.add_mem_iff_right hy').1 hu)
+end
+
 end
 
 section