Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit b018406

Browse files
sgouezelsgouezel
committed
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).
1 parent 3e32bc9 commit b018406

6 files changed

Lines changed: 181 additions & 220 deletions

File tree

‎docs/overview.yaml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -337,7 +337,7 @@ Analysis:
337337
Fubini's theorem: 'measure_theory.integral_prod'
338338
product of finitely many measures: 'measure_theory.measure.pi'
339339
convolution: 'convolution'
340-
approximation by convolution: 'cont_diff_bump_of_inner.convolution_tendsto_right'
340+
approximation by convolution: 'cont_diff_bump.convolution_tendsto_right'
341341
regularization by convolution: 'has_compact_support.cont_diff_convolution_left'
342342
change of variables formula: 'measure_theory.integral_image_eq_integral_abs_det_fderiv_smul'
343343
divergence theorem: 'measure_theory.integral_divergence_of_has_fderiv_within_at_off_countable'

‎docs/undergrad.yaml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -518,7 +518,7 @@ Measures and integral calculus:
518518
change of variables to polar co-ordinates: 'integral_comp_polar_coord_symm '
519519
change of variables to spherical co-ordinates: ''
520520
convolution: 'convolution'
521-
approximation by convolution: 'cont_diff_bump_of_inner.convolution_tendsto_right'
521+
approximation by convolution: 'cont_diff_bump.convolution_tendsto_right'
522522
regularization by convolution: 'has_compact_support.cont_diff_convolution_left'
523523
Fourier analysis:
524524
Fourier series of locally integrable periodic real-valued functions: 'fourier_basis'

‎src/analysis/calculus/bump_function_findim.lean‎

Lines changed: 4 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2022 Sébastien Gouëzel. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Sébastien Gouëzel
55
-/
6-
import analysis.calculus.specific_functions
6+
import analysis.calculus.bump_function_inner
77
import analysis.calculus.series
88
import analysis.convolution
99
import data.set.pointwise.support
@@ -16,9 +16,8 @@ Let `E` be a finite-dimensional real normed vector space. We show that any open
1616
exactly the support of a smooth function taking values in `[0, 1]`,
1717
in `is_open.exists_smooth_support_eq`.
1818
19-
TODO: use this construction to construct bump functions with nice behavior in any finite-dimensional
20-
real normed vector space, by convolving the indicator function of `closed_ball 0 1` with a
21-
function as above with `s = ball 0 D`.
19+
Then we use this construction to construct bump functions with nice behavior, by convolving
20+
the indicator function of `closed_ball 0 1` with a function as above with `s = ball 0 D`.
2221
-/
2322

2423
noncomputable theory
@@ -41,7 +40,7 @@ theorem exists_smooth_tsupport_subset {s : set E} {x : E} (hs : s ∈ 𝓝 x) :
4140
begin
4241
obtain ⟨d, d_pos, hd⟩ : ∃ (d : ℝ) (hr : 0 < d), euclidean.closed_ball x d ⊆ s,
4342
from euclidean.nhds_basis_closed_ball.mem_iff.1 hs,
44-
let c : cont_diff_bump_of_inner (to_euclidean x) :=
43+
let c : cont_diff_bump (to_euclidean x) :=
4544
{ r := d/2,
4645
R := d,
4746
r_pos := half_pos d_pos,
@@ -478,25 +477,6 @@ variable {E}
478477

479478
end helper_definitions
480479

481-
/-- The base function from which one will construct a family of bump functions. One could
482-
add more properties if they are useful and satisfied in the examples of inner product spaces
483-
and finite dimensional vector spaces, notably derivative norm control in terms of `R - 1`.
484-
TODO: move to the right file and use this to refactor bump functions in general. -/
485-
@[nolint has_nonempty_instance]
486-
structure _root_.cont_diff_bump_base (E : Type*) [normed_add_comm_group E] [normed_space ℝ E] :=
487-
(to_fun : ℝ → E → ℝ)
488-
(mem_Icc : ∀ (R : ℝ) (x : E), to_fun R x ∈ Icc (0 : ℝ) 1)
489-
(symmetric : ∀ (R : ℝ) (x : E), to_fun R (-x) = to_fun R x)
490-
(smooth : cont_diff_on ℝ ⊤ (uncurry to_fun) ((Ioi (1 : ℝ)) ×ˢ (univ : set E)))
491-
(eq_one : ∀ (R : ℝ) (hR : 1 < R) (x : E) (hx : ‖x‖ ≤ 1), to_fun R x = 1)
492-
(support : ∀ (R : ℝ) (hR : 1 < R), support (to_fun R) = metric.ball (0 : E) R)
493-
494-
/-- A class registering that a real vector space admits bump functions. This will be instantiated
495-
first for inner product spaces, and then for finite-dimensional normed spaces.
496-
We use a specific class instead of `nonempty (cont_diff_bump_base E)` for performance reasons. -/
497-
class _root_.has_cont_diff_bump (E : Type*) [normed_add_comm_group E] [normed_space ℝ E] : Prop :=
498-
(out : nonempty (cont_diff_bump_base E))
499-
500480
@[priority 100]
501481
instance {E : Type*} [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] :
502482
has_cont_diff_bump E :=

0 commit comments

Comments
 (0)