# mathlib3documentation

analysis.calculus.bump_function_findim

# Bump functions in finite-dimensional vector spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Let E be a finite-dimensional real normed vector space. We show that any open set s in E is exactly the support of a smooth function taking values in [0, 1], in is_open.exists_smooth_support_eq.

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.

theorem exists_smooth_tsupport_subset {E : Type u_1} [ E] {s : set E} {x : E} (hs : s nhds x) :
(f : E ), s f 1 f x = 1

If a set s is a neighborhood of x, then there exists a smooth function f taking values in [0, 1], supported in s and with f x = 1.

theorem is_open.exists_smooth_support_eq {E : Type u_1} [ E] {s : set E} (hs : is_open s) :
(f : E ), f 1

Given an open set s in a finite-dimensional real normed vector space, there exists a smooth function with values in [0, 1] whose support is exactly s.

noncomputable def exists_cont_diff_bump_base.φ {E : Type u_1}  :

An auxiliary function to construct partitions of unity on finite-dimensional real vector spaces. It is the characteristic function of the closed unit ball.

Equations
theorem exists_cont_diff_bump_base.u_exists (E : Type u_1) [ E]  :
(u : E ), u ( (x : E), u x 1) (x : E), u (-x) = u x
noncomputable def exists_cont_diff_bump_base.u {E : Type u_1} [ E] (x : E) :

An auxiliary function to construct partitions of unity on finite-dimensional real vector spaces, which is smooth, symmetric, and with support equal to the unit ball.

Equations
theorem exists_cont_diff_bump_base.u_smooth (E : Type u_1) [ E]  :
theorem exists_cont_diff_bump_base.u_support (E : Type u_1) [ E]  :
theorem exists_cont_diff_bump_base.u_nonneg {E : Type u_1} [ E] (x : E) :
theorem exists_cont_diff_bump_base.u_le_one {E : Type u_1} [ E] (x : E) :
theorem exists_cont_diff_bump_base.u_neg {E : Type u_1} [ E] (x : E) :
noncomputable def exists_cont_diff_bump_base.W {E : Type u_1} [ E] [borel_space E] (D : ) (x : E) :

An auxiliary function to construct partitions of unity on finite-dimensional real vector spaces, which is smooth, symmetric, with support equal to the ball of radius D and integral 1.

Equations
theorem exists_cont_diff_bump_base.W_def {E : Type u_1} [ E] [borel_space E] (D : ) :
= λ (x : E), * |D| ^ fdim E)⁻¹
theorem exists_cont_diff_bump_base.W_nonneg {E : Type u_1} [ E] [borel_space E] (D : ) (x : E) :
theorem exists_cont_diff_bump_base.W_mul_φ_nonneg {E : Type u_1} [ E] [borel_space E] (D : ) (x y : E) :
theorem exists_cont_diff_bump_base.W_integral (E : Type u_1) [ E] [borel_space E] {D : } (Dpos : 0 < D) :
theorem exists_cont_diff_bump_base.W_support (E : Type u_1) [ E] [borel_space E] {D : } (Dpos : 0 < D) :
theorem exists_cont_diff_bump_base.W_compact_support (E : Type u_1) [ E] [borel_space E] {D : } (Dpos : 0 < D) :
noncomputable def exists_cont_diff_bump_base.Y {E : Type u_1} [ E] [borel_space E] (D : ) :

An auxiliary function to construct partitions of unity on finite-dimensional real vector spaces. It is the convolution between a smooth function of integral 1 supported in the ball of radius D, with the indicator function of the closed unit ball. Therefore, it is smooth, equal to 1 on the ball of radius 1 - D, with support equal to the ball of radius 1 + D.

Equations
theorem exists_cont_diff_bump_base.Y_neg {E : Type u_1} [ E] [borel_space E] (D : ) (x : E) :
theorem exists_cont_diff_bump_base.Y_eq_one_of_mem_closed_ball {E : Type u_1} [ E] [borel_space E] {D : } {x : E} (Dpos : 0 < D) (hx : x (1 - D)) :
theorem exists_cont_diff_bump_base.Y_eq_zero_of_not_mem_ball {E : Type u_1} [ E] [borel_space E] {D : } {x : E} (Dpos : 0 < D) (hx : x (1 + D)) :
theorem exists_cont_diff_bump_base.Y_nonneg {E : Type u_1} [ E] [borel_space E] (D : ) (x : E) :
theorem exists_cont_diff_bump_base.Y_le_one {E : Type u_1} [ E] [borel_space E] {D : } (x : E) (Dpos : 0 < D) :
theorem exists_cont_diff_bump_base.Y_pos_of_mem_ball {E : Type u_1} [ E] [borel_space E] {D : } {x : E} (Dpos : 0 < D) (D_lt_one : D < 1) (hx : x (1 + D)) :
theorem exists_cont_diff_bump_base.Y_support (E : Type u_1) [ E] [borel_space E] {D : } (Dpos : 0 < D) (D_lt_one : D < 1) :
@[protected, instance]