feat(analysis/calculus/special_functions): refactor bump functions (#…

…17453)

Currently, we have satisfactory bump functions on inner spaces (equal to 1 on `ball c r` and support equal to `ball c R`), and less satisfactory bump functions on general finite-dimensional normed spaces (equal to 1 on a neighborhood of `c`, with support a larger neighborhood of `c`), where the latter are obtained from the former by composing with an arbitrary linear equiv with an inner product space called `to_euclidean`. In particular, they have different names (`bump_function_of_inner` and `bump_function`) and whenever one wants to prove properties of `bump_function` one has to juggle with the `to_euclidean`.

We refactor bump functions to get a coherent theory, which is uniform over all normed spaces. We remove completely `bump_function_of_inner`, and we make sure that `bump_function c r R` is a smooth function equal to `1` on `ball c r` and with support exactly `ball c R`, on all normed spaces. 

For this, we provide a typeclass `has_cont_diff_bump` saying that a space has nice bump functions, and we instantiate it both on inner product spaces (using the old approach with a function constructed from the norm and from `exp(-1/x^2)`), and on finite-dimensional normed spaces (where the bump functions have already been constructed by convolution in #18095).

docs/overview.yaml

@@ -337,7 +337,7 @@ Analysis:
     Fubini's theorem: 'measure_theory.integral_prod'
     product of finitely many measures: 'measure_theory.measure.pi'
     convolution: 'convolution'
-    approximation by convolution: 'cont_diff_bump_of_inner.convolution_tendsto_right'
+    approximation by convolution: 'cont_diff_bump.convolution_tendsto_right'
     regularization by convolution: 'has_compact_support.cont_diff_convolution_left'
     change of variables formula: 'measure_theory.integral_image_eq_integral_abs_det_fderiv_smul'
     divergence theorem: 'measure_theory.integral_divergence_of_has_fderiv_within_at_off_countable'

docs/undergrad.yaml

@@ -518,7 +518,7 @@ Measures and integral calculus:
     change of variables to polar co-ordinates: 'integral_comp_polar_coord_symm '
     change of variables to spherical co-ordinates: ''
     convolution: 'convolution'
-    approximation by convolution: 'cont_diff_bump_of_inner.convolution_tendsto_right'
+    approximation by convolution: 'cont_diff_bump.convolution_tendsto_right'
     regularization by convolution: 'has_compact_support.cont_diff_convolution_left'
   Fourier analysis:
     Fourier series of locally integrable periodic real-valued functions: 'fourier_basis'

src/analysis/calculus/bump_function_findim.lean

@@ -3,7 +3,7 @@ Copyright (c) 2022 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
-import analysis.calculus.specific_functions
+import analysis.calculus.bump_function_inner
 import analysis.calculus.series
 import analysis.convolution
 import data.set.pointwise.support
@@ -16,9 +16,8 @@ Let `E` be a finite-dimensional real normed vector space. We show that any open
 exactly the support of a smooth function taking values in `[0, 1]`,
 in `is_open.exists_smooth_support_eq`.
 
-TODO: use this construction to construct bump functions with nice behavior in any finite-dimensional
-real normed vector space, by convolving the indicator function of `closed_ball 0 1` with a
-function as above with `s = ball 0 D`.
+Then we use this construction to construct bump functions with nice behavior, by convolving
+the indicator function of `closed_ball 0 1` with a function as above with `s = ball 0 D`.
 -/
 
 noncomputable theory
@@ -41,7 +40,7 @@ theorem exists_smooth_tsupport_subset {s : set E} {x : E} (hs : s ∈ 𝓝 x) :
 begin
   obtain ⟨d, d_pos, hd⟩ : ∃ (d : ℝ) (hr : 0 < d), euclidean.closed_ball x d ⊆ s,
     from euclidean.nhds_basis_closed_ball.mem_iff.1 hs,
-  let c : cont_diff_bump_of_inner (to_euclidean x) :=
+  let c : cont_diff_bump (to_euclidean x) :=
   { r := d/2,
     R := d,
     r_pos := half_pos d_pos,
@@ -478,25 +477,6 @@ variable {E}
 
 end helper_definitions
 
-/-- The base function from which one will construct a family of bump functions. One could
-add more properties if they are useful and satisfied in the examples of inner product spaces
-and finite dimensional vector spaces, notably derivative norm control in terms of `R - 1`.
-TODO: move to the right file and use this to refactor bump functions in general. -/
-@[nolint has_nonempty_instance]
-structure _root_.cont_diff_bump_base (E : Type*) [normed_add_comm_group E] [normed_space ℝ E] :=
-(to_fun : ℝ → E → ℝ)
-(mem_Icc   : ∀ (R : ℝ) (x : E), to_fun R x ∈ Icc (0 : ℝ) 1)
-(symmetric : ∀ (R : ℝ) (x : E), to_fun R (-x) = to_fun R x)
-(smooth    : cont_diff_on ℝ ⊤ (uncurry to_fun) ((Ioi (1 : ℝ)) ×ˢ (univ : set E)))
-(eq_one    : ∀ (R : ℝ) (hR : 1 < R) (x : E) (hx : ‖x‖ ≤ 1), to_fun R x = 1)
-(support   : ∀ (R : ℝ) (hR : 1 < R), support (to_fun R) = metric.ball (0 : E) R)
-
-/-- A class registering that a real vector space admits bump functions. This will be instantiated
-first for inner product spaces, and then for finite-dimensional normed spaces.
-We use a specific class instead of `nonempty (cont_diff_bump_base E)` for performance reasons. -/
-class _root_.has_cont_diff_bump (E : Type*) [normed_add_comm_group E] [normed_space ℝ E] : Prop :=
-(out : nonempty (cont_diff_bump_base E))
-
 @[priority 100]
 instance {E : Type*} [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] :
   has_cont_diff_bump E :=