feat(geometry/manifold/bump_function): define smooth bump functions, …

…baby version of the Whitney embedding thm (#6839)

* refactor some functions in `analysis/calculus/specific_functions` to use bundled structures;
* define `to_euclidean`, `euclidean.dist`, `euclidean.ball`, and `euclidean.closed_ball`;
* define smooth bump functions on manifolds;
* prove a baby version of the Whitney embedding theorem.

src/analysis/calculus/specific_functions.lean

@@ -6,7 +6,7 @@ Authors: Sébastien Gouëzel
 import analysis.calculus.extend_deriv
 import analysis.calculus.iterated_deriv
 import analysis.special_functions.exp_log
-import analysis.normed_space.inner_product
+import analysis.normed_space.euclidean_dist
 import topology.algebra.polynomial
 
 /-!
@@ -17,16 +17,36 @@ function cannot have:
 
 * `exp_neg_inv_glue` is equal to zero for `x ≤ 0` and is strictly positive otherwise; it is given by
   `x ↦ exp (-1/x)` for `x > 0`;
-* `smooth_transition` is equal to zero for `x ≤ 0` and is equal to one for `x ≥ 1`; it is given by
-  `exp_neg_inv_glue x / (exp_neg_inv_glue x + exp_neg_inv_glue (1 - x))`;
-* `smooth_bump_function` is equal to one on the closed ball of radius `1` and is equal to `0`
-  outside of the open ball of radius `2`.
+
+* `real.smooth_transition` is equal to zero for `x ≤ 0` and is equal to one for `x ≥ 1`; it is given
+  by `exp_neg_inv_glue x / (exp_neg_inv_glue x + exp_neg_inv_glue (1 - x))`;
+
+* `f : times_cont_diff_bump_of_inner c`, where `c` is a point in an inner product space, is
+  a bundled smooth function such that
+
+  - `f` is equal to `1` in `metric.closed_ball c f.r`;
+  - `support f = metric.ball c f.R`;
+  - `0 ≤ f x ≤ 1` for all `x`.
+
+  The structure `times_cont_diff_bump_of_inner` contains the data required to construct the
+  function: real numbers `r`, `R`, and proofs of `0 < r < R`. The function itself is available
+  through `coe_fn`.
+
+* `f : times_cont_diff_bump c`, where `c` is a point in a finite dimensional real vector space, is a
+  bundled smooth function such that
+
+  - `f` is equal to `1` in `euclidean.closed_ball c f.r`;
+  - `support f = euclidean.ball c f.R`;
+  - `0 ≤ f x ≤ 1` for all `x`.
+
+  The structure `times_cont_diff_bump` contains the data required to construct the function: real
+  numbers `r`, `R`, and proofs of `0 < r < R`. The function itself is available through `coe_fn`.
 -/
 
 noncomputable theory
 open_locale classical topological_space
 
-open polynomial real filter set
+open polynomial real filter set function
 
 /-- `exp_neg_inv_glue` is the real function given by `x ↦ exp (-1/x)` for `x > 0` and `0`
 for `x ≤ 0`. It is a basic building block to construct smooth partitions of unity. Its main property
@@ -197,9 +217,11 @@ end exp_neg_inv_glue
 
 /-- An infinitely smooth function `f : ℝ → ℝ` such that `f x = 0` for `x ≤ 0`,
 `f x = 1` for `1 ≤ x`, and `0 < f x < 1` for `0 < x < 1`. -/
-def smooth_transition (x : ℝ) : ℝ :=
+def real.smooth_transition (x : ℝ) : ℝ :=
 exp_neg_inv_glue x / (exp_neg_inv_glue x + exp_neg_inv_glue (1 - x))
 
+namespace real
+
 namespace smooth_transition
 
 variables {x : ℝ}
@@ -240,86 +262,190 @@ smooth_transition.times_cont_diff.times_cont_diff_at
 
 end smooth_transition
 
-variables {E : Type*}
+end real
+
+variable {E : Type*}
+
+/-- `f : times_cont_diff_bump_of_inner c`, where `c` is a point in an inner product space, is a
+bundled smooth function such that
+
+- `f` is equal to `1` in `metric.closed_ball c f.r`;
+- `support f = metric.ball c f.R`;
+- `0 ≤ f x ≤ 1` for all `x`.
+
+The structure `times_cont_diff_bump_of_inner` contains the data required to construct the function:
+real numbers `r`, `R`, and proofs of `0 < r < R`. The function itself is available through
+`coe_fn`. -/
+structure times_cont_diff_bump_of_inner (c : E) :=
+(r R : ℝ)
+(r_pos : 0 < r)
+(r_lt_R : r < R)
 
-/-- Let `x` be a point of a real inner product space; let `0 < r < R` be real numbers.
-Then `smooth_bump_function x r R` is a function `E → ℝ` with the following properties:
+namespace times_cont_diff_bump_of_inner
 
-- `smooth_bump_function x r R` is infinitely smooth on `E`;
-- `smooth_bump_function x r R` is equal to `1` on `closed_ball x r`;
-- `0 < smooth_bump_function x r R y < 1` if `r < dist y x < R`;
-- `smooth_bump_function x r R y = 0` if `R ≤ dist y x.
+lemma R_pos {c : E} (f : times_cont_diff_bump_of_inner c) : 0 < f.R := f.r_pos.trans f.r_lt_R
 
-We define this function for any `x`, `r`, and `R`  -/
-def smooth_bump_function [inner_product_space ℝ E] (x : E) (r R : ℝ) (y : E) : ℝ :=
-smooth_transition ((R - dist y x) / (R - r))
+instance (c : E) : inhabited (times_cont_diff_bump_of_inner c) := ⟨⟨1, 2, zero_lt_one, one_lt_two⟩⟩
 
-namespace smooth_bump_function
+variables [inner_product_space ℝ E] {c : E} (f : times_cont_diff_bump_of_inner c) {x : E}
 
-variables [inner_product_space ℝ E] {r R : ℝ} {x y : E}
+/-- The function defined by `f : times_cont_diff_bump_of_inner c`. Use automatic coercion to
+function instead. -/
+def to_fun (f : times_cont_diff_bump_of_inner c) : E → ℝ :=
+λ x, real.smooth_transition ((f.R - dist x c) / (f.R - f.r))
 
-open smooth_transition metric
+instance : has_coe_to_fun (times_cont_diff_bump_of_inner c) := ⟨_, to_fun⟩
 
-lemma one_of_mem_closed_ball (hy : y ∈ closed_ball x r) (hrR : r < R) :
-  smooth_bump_function x r R y = 1 :=
-one_of_one_le $ (one_le_div (sub_pos.2 hrR)).2 $ sub_le_sub_left hy _
+open real (smooth_transition) real.smooth_transition metric
 
-lemma nonneg : 0 ≤ smooth_bump_function x r R y :=
-nonneg _
+lemma one_of_mem_closed_ball (hx : x ∈ closed_ball c f.r) :
+  f x = 1 :=
+one_of_one_le $ (one_le_div (sub_pos.2 f.r_lt_R)).2 $ sub_le_sub_left hx _
 
-lemma le_one : smooth_bump_function x r R y ≤ 1 :=
-le_one _
+lemma nonneg : 0 ≤ f x := nonneg _
 
-lemma pos_of_mem_ball (hx : y ∈ ball x R) (hrR : r < R) :
-  0 < smooth_bump_function x r R y :=
-pos_of_pos $ div_pos (sub_pos.2 hx) (sub_pos.2 hrR)
+lemma le_one : f x ≤ 1 := le_one _
 
-lemma lt_one_of_lt_dist (h : r < dist y x) (hrR : r < R) : smooth_bump_function x r R y < 1 :=
-lt_one_of_lt_one $ (div_lt_one (sub_pos.2 hrR)).2 $ sub_lt_sub_left h _
+lemma pos_of_mem_ball (hx : x ∈ ball c f.R) : 0 < f x :=
+pos_of_pos $ div_pos (sub_pos.2 hx) (sub_pos.2 f.r_lt_R)
 
-lemma zero_of_le_dist (hx : R ≤ dist y x) (hrR : r ≤ R) : smooth_bump_function x r R y = 0 :=
-zero_of_nonpos $ div_nonpos_of_nonpos_of_nonneg (sub_nonpos.2 hx) (sub_nonneg.2 hrR)
+lemma lt_one_of_lt_dist (h : f.r < dist x c) : f x < 1 :=
+lt_one_of_lt_one $ (div_lt_one (sub_pos.2 f.r_lt_R)).2 $ sub_lt_sub_left h _
 
-lemma support_eq (hrR : r < R) :
-  function.support (smooth_bump_function x r R : E → ℝ) = metric.ball x R :=
+lemma zero_of_le_dist (hx : f.R ≤ dist x c) : f x = 0 :=
+zero_of_nonpos $ div_nonpos_of_nonpos_of_nonneg (sub_nonpos.2 hx) (sub_nonneg.2 f.r_lt_R.le)
+
+lemma support_eq : support ⇑f = metric.ball c f.R :=
 begin
-  ext y,
-  suffices : smooth_bump_function x r R y ≠ 0 ↔ dist y x < R, by simpa [function.mem_support],
-  cases lt_or_le (dist y x) R with hx hx,
-  { simp [hx, (pos_of_mem_ball hx hrR).ne'] },
-  { simp [hx.not_lt, zero_of_le_dist hx hrR.le] }
+  ext x,
+  suffices : f x ≠ 0 ↔ dist x c < f.R, by simpa [mem_support],
+  cases lt_or_le (dist x c) f.R with hx hx,
+  { simp [hx, (f.pos_of_mem_ball hx).ne'] },
+  { simp [hx.not_lt, f.zero_of_le_dist hx] }
 end
 
-lemma eventually_eq_one_of_mem_ball (h : y ∈ ball x r) (hrR : r < R) :
-  smooth_bump_function x r R =ᶠ[𝓝 y] (λ _, 1) :=
+lemma eventually_eq_one_of_mem_ball (h : x ∈ ball c f.r) :
+  f =ᶠ[𝓝 x] 1 :=
 ((is_open_lt (continuous_id.dist continuous_const) continuous_const).eventually_mem h).mono $
-  λ z hz, one_of_mem_closed_ball (le_of_lt hz) hrR
+  λ z hz, f.one_of_mem_closed_ball (le_of_lt hz)
 
-lemma eventually_eq_one (h0 : 0 < r) (hrR : r < R) :
-  smooth_bump_function x r R =ᶠ[𝓝 (x : E)] (λ _, 1) :=
-eventually_eq_one_of_mem_ball (mem_ball_self h0) hrR
+lemma eventually_eq_one : f =ᶠ[𝓝 c] 1 :=
+f.eventually_eq_one_of_mem_ball (mem_ball_self f.r_pos)
 
-protected lemma times_cont_diff_at (h0 : 0 < r) (hrR : r < R) {n} :
-  times_cont_diff_at ℝ n (smooth_bump_function x r R) y :=
+protected lemma times_cont_diff_at {n} :
+  times_cont_diff_at ℝ n f x :=
 begin
-  rcases em (y = x) with rfl|hx,
-  { exact times_cont_diff_at_const.congr_of_eventually_eq (eventually_eq_one h0 hrR) },
-  { exact smooth_transition.times_cont_diff_at.comp y
+  rcases em (x = c) with rfl|hx,
+  { refine times_cont_diff_at.congr_of_eventually_eq _ f.eventually_eq_one,
+    rw pi.one_def,
+    exact times_cont_diff_at_const },
+  { exact real.smooth_transition.times_cont_diff_at.comp x
       (times_cont_diff_at.div_const $ times_cont_diff_at_const.sub $
         times_cont_diff_at_id.dist times_cont_diff_at_const hx) }
 end
 
-protected lemma times_cont_diff (h0 : 0 < r) (hrR : r < R) {n} :
-  times_cont_diff ℝ n (smooth_bump_function x r R) :=
-times_cont_diff_iff_times_cont_diff_at.2 $ λ y, smooth_bump_function.times_cont_diff_at h0 hrR
+protected lemma times_cont_diff {n} :
+  times_cont_diff ℝ n f :=
+times_cont_diff_iff_times_cont_diff_at.2 $ λ y, f.times_cont_diff_at
+
+protected lemma times_cont_diff_within_at {s n} :
+  times_cont_diff_within_at ℝ n f s x :=
+f.times_cont_diff_at.times_cont_diff_within_at
+
+end times_cont_diff_bump_of_inner
+
+/-- `f : times_cont_diff_bump c`, where `c` is a point in a finite dimensional real vector space, is
+a bundled smooth function such that
+
+  - `f` is equal to `1` in `euclidean.closed_ball c f.r`;
+  - `support f = euclidean.ball c f.R`;
+  - `0 ≤ f x ≤ 1` for all `x`.
+
+The structure `times_cont_diff_bump` contains the data required to construct the function: real
+numbers `r`, `R`, and proofs of `0 < r < R`. The function itself is available through `coe_fn`.-/
+structure times_cont_diff_bump [normed_group E] [normed_space ℝ E] [finite_dimensional ℝ E] (c : E)
+  extends times_cont_diff_bump_of_inner (to_euclidean c)
+
+namespace times_cont_diff_bump
+
+variables [normed_group E] [normed_space ℝ E] [finite_dimensional ℝ E] {c x : E}
+  (f : times_cont_diff_bump c)
+
+/-- The function defined by `f : times_cont_diff_bump c`. Use automatic coercion to function
+instead. -/
+def to_fun (f : times_cont_diff_bump c) : E → ℝ := f.to_times_cont_diff_bump_of_inner ∘ to_euclidean
+
+instance : has_coe_to_fun (times_cont_diff_bump c) :=
+⟨λ f, E → ℝ, to_fun⟩
+
+instance (c : E) : inhabited (times_cont_diff_bump c) := ⟨⟨default _⟩⟩
 
-protected lemma times_cont_diff_within_at (h0 : 0 < r) (hrR : r < R) {s n} :
-  times_cont_diff_within_at ℝ n (smooth_bump_function x r R) s y :=
-(smooth_bump_function.times_cont_diff_at h0 hrR).times_cont_diff_within_at
+lemma R_pos : 0 < f.R := f.to_times_cont_diff_bump_of_inner.R_pos
 
-end smooth_bump_function
+lemma coe_eq_comp : ⇑f = f.to_times_cont_diff_bump_of_inner ∘ to_euclidean := rfl
 
-open function finite_dimensional metric
+lemma one_of_mem_closed_ball (hx : x ∈ euclidean.closed_ball c f.r) :
+  f x = 1 :=
+f.to_times_cont_diff_bump_of_inner.one_of_mem_closed_ball hx
+
+lemma nonneg : 0 ≤ f x := f.to_times_cont_diff_bump_of_inner.nonneg
+
+lemma le_one : f x ≤ 1 := f.to_times_cont_diff_bump_of_inner.le_one
+
+lemma pos_of_mem_ball (hx : x ∈ euclidean.ball c f.R) : 0 < f x :=
+f.to_times_cont_diff_bump_of_inner.pos_of_mem_ball hx
+
+lemma lt_one_of_lt_dist (h : f.r < euclidean.dist x c) : f x < 1 :=
+f.to_times_cont_diff_bump_of_inner.lt_one_of_lt_dist h
+
+lemma zero_of_le_dist (hx : f.R ≤ euclidean.dist x c) : f x = 0 :=
+f.to_times_cont_diff_bump_of_inner.zero_of_le_dist hx
+
+lemma support_eq : support ⇑f = euclidean.ball c f.R :=
+by rw [euclidean.ball_eq_preimage, ← f.to_times_cont_diff_bump_of_inner.support_eq,
+  ← support_comp_eq_preimage, coe_eq_comp]
+
+lemma closure_support_eq : closure (support f) = euclidean.closed_ball c f.R :=
+by rw [f.support_eq, euclidean.closure_ball _ f.R_pos]
+
+lemma compact_closure_support : is_compact (closure (support f)) :=
+by { rw f.closure_support_eq, exact euclidean.compact_ball }
+
+lemma eventually_eq_one_of_mem_ball (h : x ∈ euclidean.ball c f.r) :
+  f =ᶠ[𝓝 x] 1 :=
+to_euclidean.continuous_at (f.to_times_cont_diff_bump_of_inner.eventually_eq_one_of_mem_ball h)
+
+lemma eventually_eq_one : f =ᶠ[𝓝 c] 1 :=
+f.eventually_eq_one_of_mem_ball $ euclidean.mem_ball_self f.r_pos
+
+protected lemma times_cont_diff {n} :
+  times_cont_diff ℝ n f :=
+f.to_times_cont_diff_bump_of_inner.times_cont_diff.comp (to_euclidean : E ≃L[ℝ] _).times_cont_diff
+
+protected lemma times_cont_diff_at {n} :
+  times_cont_diff_at ℝ n f x :=
+f.times_cont_diff.times_cont_diff_at
+
+protected lemma times_cont_diff_within_at {s n} :
+  times_cont_diff_within_at ℝ n f s x :=
+f.times_cont_diff_at.times_cont_diff_within_at
+
+lemma exists_closure_support_subset {s : set E} (hs : s ∈ 𝓝 c) :
+  ∃ f : times_cont_diff_bump c, closure (support f) ⊆ s :=
+let ⟨R, h0, hR⟩ := euclidean.nhds_basis_closed_ball.mem_iff.1 hs
+in ⟨⟨⟨R / 2, R, half_pos h0, half_lt_self h0⟩⟩, by rwa closure_support_eq⟩
+
+lemma exists_closure_subset {R : ℝ} (hR : 0 < R)
+  {s : set E} (hs : is_closed s) (hsR : s ⊆ euclidean.ball c R) :
+  ∃ f : times_cont_diff_bump c, f.R = R ∧ s ⊆ euclidean.ball c f.r :=
+begin
+  rcases euclidean.exists_pos_lt_subset_ball hR hs hsR with ⟨r, hr, hsr⟩,
+  exact ⟨⟨⟨r, R, hr.1, hr.2⟩⟩, rfl, hsr⟩
+end
+
+end times_cont_diff_bump
+
+open finite_dimensional metric
 
 /-- If `E` is a finite dimensional normed space over `ℝ`, then for any point `x : E` and its
 neighborhood `s` there exists an infinitely smooth function with the following properties:
@@ -328,27 +454,13 @@ neighborhood `s` there exists an infinitely smooth function with the following p
 * `f y = 0` outside of `s`;
 *  moreover, `closure (support f) ⊆ s` and `closure (support f)` is a compact set;
 * `f y ∈ [0, 1]` for all `y`.
--/
+
+This lemma is a simple wrapper around lemmas about bundled smooth bump functions, see
+`times_cont_diff_bump`. -/
 lemma exists_times_cont_diff_bump_function_of_mem_nhds [normed_group E] [normed_space ℝ E]
   [finite_dimensional ℝ E] {x : E} {s : set E} (hs : s ∈ 𝓝 x) :
   ∃ f : E → ℝ, f =ᶠ[𝓝 x] 1 ∧ (∀ y, f y ∈ Icc (0 : ℝ) 1) ∧ times_cont_diff ℝ ⊤ f ∧
     is_compact (closure $ support f) ∧ closure (support f) ⊆ s :=
-begin
-  have e : E ≃L[ℝ] euclidean_space ℝ (fin $ findim ℝ E) :=
-    continuous_linear_equiv.of_findim_eq findim_euclidean_space_fin.symm,
-  rcases locally_compact_space.local_compact_nhds _ _ hs with ⟨K, hxK, hKs, hKc⟩,
-  rw [← e.symm_map_nhds_eq, mem_map] at hxK,
-  obtain ⟨R, hR₀, hR⟩ : ∃ R > 0, ∀ y ∈ ball (e x) R, e.symm y ∈ K, from mem_nhds_iff.1 hxK,
-  have Hpos : 0 < R / 2 := half_pos hR₀,
-  have Hlt : R / 2 < R := half_lt_self hR₀,
-  have : support (smooth_bump_function (e x) (R / 2) R ∘ e) ⊆ K,
-  { intros y hy,
-    rw [support_comp_eq_preimage, smooth_bump_function.support_eq Hlt] at hy,
-    simpa only [e.symm_apply_apply] using (hR _ hy) },
-  exact ⟨smooth_bump_function (e x) (R / 2) R ∘ e,
-    e.continuous_at.eventually (smooth_bump_function.eventually_eq_one Hpos Hlt),
-    λ y, ⟨smooth_bump_function.nonneg, smooth_bump_function.le_one⟩,
-    (smooth_bump_function.times_cont_diff Hpos Hlt).comp e.times_cont_diff,
-    compact_closure_of_subset_compact hKc this,
-    subset.trans (closure_minimal this hKc.is_closed) hKs⟩
-end
+let ⟨f, hf⟩ := times_cont_diff_bump.exists_closure_support_subset hs in
+⟨f, f.eventually_eq_one, λ y, ⟨f.nonneg, f.le_one⟩, f.times_cont_diff,
+  f.compact_closure_support, hf⟩