# mathlibdocumentation

analysis.calculus.specific_functions

# Infinitely smooth bump function #

In this file we construct several infinitely smooth functions with properties that an analytic 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;

• 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.

def exp_neg_inv_glue (x : ) :

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 is that it vanishes for x ≤ 0, it is positive for x > 0, and the junction between the two behaviors is flat enough to retain smoothness. The fact that this function is C^∞ is proved in exp_neg_inv_glue.smooth.

Equations

Our goal is to prove that exp_neg_inv_glue is C^∞. For this, we compute its successive derivatives for x > 0. The n-th derivative is of the form P_aux n (x) exp(-1/x) / x^(2 n), where P_aux n is computed inductively.

Equations
def exp_neg_inv_glue.f_aux (n : ) (x : ) :

Formula for the n-th derivative of exp_neg_inv_glue, as an auxiliary function f_aux.

Equations

The 0-th auxiliary function f_aux 0 coincides with exp_neg_inv_glue, by definition.

theorem exp_neg_inv_glue.f_aux_deriv (n : ) (x : ) (hx : x 0) :
has_deriv_at (λ (x : ), * real.exp (-x⁻¹) / x ^ 2 * n) (exp_neg_inv_glue.P_aux (n + 1))) * real.exp (-x⁻¹) / x ^ 2 * (n + 1)) x

For positive values, the derivative of the n-th auxiliary function f_aux n (given in this statement in unfolded form) is the n+1-th auxiliary function, since the polynomial P_aux (n+1) was chosen precisely to ensure this.

theorem exp_neg_inv_glue.f_aux_deriv_pos (n : ) (x : ) (hx : 0 < x) :
(exp_neg_inv_glue.P_aux (n + 1))) * real.exp (-x⁻¹) / x ^ 2 * (n + 1)) x

For positive values, the derivative of the n-th auxiliary function f_aux n is the n+1-th auxiliary function.

theorem exp_neg_inv_glue.f_aux_limit (n : ) :
filter.tendsto (λ (x : ), * real.exp (-x⁻¹) / x ^ 2 * n) (𝓝[] 0) (𝓝 0)

To get differentiability at 0 of the auxiliary functions, we need to know that their limit is 0, to be able to apply general differentiability extension theorems. This limit is checked in this lemma.

Deduce from the limiting behavior at 0 of its derivative and general differentiability extension theorems that the auxiliary function f_aux n is differentiable at 0, with derivative 0.

At every point, the auxiliary function f_aux n has a derivative which is equal to f_aux (n+1).

The successive derivatives of the auxiliary function f_aux 0 are the functions f_aux n, by induction.

The function exp_neg_inv_glue is smooth.

theorem exp_neg_inv_glue.zero_of_nonpos {x : } (hx : x 0) :

The function exp_neg_inv_glue vanishes on (-∞, 0].

theorem exp_neg_inv_glue.pos_of_pos {x : } (hx : 0 < x) :

The function exp_neg_inv_glue is positive on (0, +∞).

theorem exp_neg_inv_glue.nonneg (x : ) :

The function exp_neg_inv_glue is nonnegative.

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.

Equations
theorem real.smooth_transition.one_of_one_le {x : } (h : 1 x) :
theorem real.smooth_transition.pos_of_pos {x : } (h : 0 < x) :
structure times_cont_diff_bump_of_inner {E : Type u_1} (c : E) :
Type
• r :
• R :
• r_pos : 0 < self.r
• r_lt_R : self.r < self.R

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.

theorem times_cont_diff_bump_of_inner.R_pos {E : Type u_1} {c : E}  :
0 < f.R
@[instance]
def times_cont_diff_bump_of_inner.inhabited {E : Type u_1} (c : E) :
Equations
def times_cont_diff_bump_of_inner.to_fun {E : Type u_1} {c : E}  :
E →

The function defined by f : times_cont_diff_bump_of_inner c. Use automatic coercion to function instead.

Equations
@[instance]
def times_cont_diff_bump_of_inner.has_coe_to_fun {E : Type u_1} {c : E} :
Equations
theorem times_cont_diff_bump_of_inner.one_of_mem_closed_ball {E : Type u_1} {c : E} {x : E} (hx : x ) :
f x = 1
theorem times_cont_diff_bump_of_inner.nonneg {E : Type u_1} {c : E} {x : E} :
0 f x
theorem times_cont_diff_bump_of_inner.le_one {E : Type u_1} {c : E} {x : E} :
f x 1
theorem times_cont_diff_bump_of_inner.pos_of_mem_ball {E : Type u_1} {c : E} {x : E} (hx : x f.R) :
0 < f x
theorem times_cont_diff_bump_of_inner.lt_one_of_lt_dist {E : Type u_1} {c : E} {x : E} (h : f.r < dist x c) :
f x < 1
theorem times_cont_diff_bump_of_inner.zero_of_le_dist {E : Type u_1} {c : E} {x : E} (hx : f.R dist x c) :
f x = 0
theorem times_cont_diff_bump_of_inner.support_eq {E : Type u_1} {c : E}  :
theorem times_cont_diff_bump_of_inner.eventually_eq_one_of_mem_ball {E : Type u_1} {c : E} {x : E} (h : x f.r) :
theorem times_cont_diff_bump_of_inner.eventually_eq_one {E : Type u_1} {c : E}  :
theorem times_cont_diff_bump_of_inner.times_cont_diff_at {E : Type u_1} {c : E} {x : E} {n : with_top } :
x
theorem times_cont_diff_bump_of_inner.times_cont_diff {E : Type u_1} {c : E} {n : with_top } :
theorem times_cont_diff_bump_of_inner.times_cont_diff_within_at {E : Type u_1} {c : E} {x : E} {s : set E} {n : with_top } :
x
structure times_cont_diff_bump {E : Type u_1} [normed_group E] [ E] (c : E) :
Type
• to_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.

def times_cont_diff_bump.to_fun {E : Type u_1} [normed_group E] [ E] {c : E} (f : times_cont_diff_bump c) :
E →

The function defined by f : times_cont_diff_bump c. Use automatic coercion to function instead.

Equations
@[instance]
def times_cont_diff_bump.has_coe_to_fun {E : Type u_1} [normed_group E] [ E] {c : E} :
Equations
@[instance]
def times_cont_diff_bump.inhabited {E : Type u_1} [normed_group E] [ E] (c : E) :
Equations
theorem times_cont_diff_bump.R_pos {E : Type u_1} [normed_group E] [ E] {c : E} (f : times_cont_diff_bump c) :
theorem times_cont_diff_bump.coe_eq_comp {E : Type u_1} [normed_group E] [ E] {c : E} (f : times_cont_diff_bump c) :
theorem times_cont_diff_bump.one_of_mem_closed_ball {E : Type u_1} [normed_group E] [ E] {c x : E} (f : times_cont_diff_bump c) (hx : x ) :
f x = 1
theorem times_cont_diff_bump.nonneg {E : Type u_1} [normed_group E] [ E] {c x : E} (f : times_cont_diff_bump c) :
0 f x
theorem times_cont_diff_bump.le_one {E : Type u_1} [normed_group E] [ E] {c x : E} (f : times_cont_diff_bump c) :
f x 1
theorem times_cont_diff_bump.pos_of_mem_ball {E : Type u_1} [normed_group E] [ E] {c x : E} (f : times_cont_diff_bump c) (hx : x ) :
0 < f x
theorem times_cont_diff_bump.lt_one_of_lt_dist {E : Type u_1} [normed_group E] [ E] {c x : E} (f : times_cont_diff_bump c) (h : f.to_times_cont_diff_bump_of_inner.r < ) :
f x < 1
theorem times_cont_diff_bump.zero_of_le_dist {E : Type u_1} [normed_group E] [ E] {c x : E} (f : times_cont_diff_bump c) (hx : f.to_times_cont_diff_bump_of_inner.R ) :
f x = 0
theorem times_cont_diff_bump.support_eq {E : Type u_1} [normed_group E] [ E] {c : E} (f : times_cont_diff_bump c) :
theorem times_cont_diff_bump.closure_support_eq {E : Type u_1} [normed_group E] [ E] {c : E} (f : times_cont_diff_bump c) :
theorem times_cont_diff_bump.compact_closure_support {E : Type u_1} [normed_group E] [ E] {c : E} (f : times_cont_diff_bump c) :
theorem times_cont_diff_bump.eventually_eq_one_of_mem_ball {E : Type u_1} [normed_group E] [ E] {c x : E} (f : times_cont_diff_bump c) (h : x ) :
theorem times_cont_diff_bump.eventually_eq_one {E : Type u_1} [normed_group E] [ E] {c : E} (f : times_cont_diff_bump c) :
theorem times_cont_diff_bump.times_cont_diff {E : Type u_1} [normed_group E] [ E] {c : E} (f : times_cont_diff_bump c) {n : with_top } :
theorem times_cont_diff_bump.times_cont_diff_at {E : Type u_1} [normed_group E] [ E] {c x : E} (f : times_cont_diff_bump c) {n : with_top } :
x
theorem times_cont_diff_bump.times_cont_diff_within_at {E : Type u_1} [normed_group E] [ E] {c x : E} (f : times_cont_diff_bump c) {s : set E} {n : with_top } :
x
theorem times_cont_diff_bump.exists_closure_support_subset {E : Type u_1} [normed_group E] [ E] {c : E} {s : set E} (hs : s 𝓝 c) :
∃ (f : ,
theorem times_cont_diff_bump.exists_closure_subset {E : Type u_1} [normed_group E] [ E] {c : E} {R : } (hR : 0 < R) {s : set E} (hs : is_closed s) (hsR : s ) :
∃ (f : ,
theorem exists_times_cont_diff_bump_function_of_mem_nhds {E : Type u_1} [normed_group E] [ E] {x : E} {s : set E} (hs : s 𝓝 x) :
∃ (f : E → ), f =ᶠ[𝓝 x] 1 (∀ (y : E), f y 1) s

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:

• f y = 1 in a neighborhood of x;
• 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`.