mathlib documentation

analysis.calculus.bump_function_findim

Bump functions in finite-dimensional vector spaces #

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.

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.

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)) :
@[nolint]
structure cont_diff_bump_base (E : Type u_2) [normed_add_comm_group E] [normed_space E] :
Type u_2

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.

Instances for cont_diff_bump_base
  • cont_diff_bump_base.has_sizeof_inst
@[class]
structure has_cont_diff_bump (E : Type u_2) [normed_add_comm_group E] [normed_space E] :
Prop

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.

Instances of this typeclass