mathlib3 documentation

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.

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.

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} [normed_add_comm_group E] :

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

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

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

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_pos_of_mem_ball {E : Type u_1} [normed_add_comm_group E] [normed_space E] [finite_dimensional E] [measurable_space E] [borel_space E] {D : } {x : E} (Dpos : 0 < D) (D_lt_one : D < 1) (hx : x metric.ball 0 (1 + D)) :