# 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 IsOpen.exists_smooth_support_eq.

Then we use this construction to construct bump functions with nice behavior, by convolving the indicator function of closedBall 0 1 with a function as above with s = ball 0 D.

theorem exists_smooth_tsupport_subset {E : Type u_1} [] [] {s : Set E} {x : E} (hs : s nhds x) :
∃ (f : E), s Set.Icc 0 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 IsOpen.exists_smooth_support_eq {E : Type u_1} [] [] {s : Set E} (hs : ) :
∃ (f : E), Set.Icc 0 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.

def ExistsContDiffBumpBase.φ {E : Type u_1} :
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
• ExistsContDiffBumpBase.φ = ().indicator fun (x : E) => 1
Instances For
theorem ExistsContDiffBumpBase.u_exists (E : Type u_1) [] [] :
∃ (u : E), (∀ (x : E), u x Set.Icc 0 1) ∀ (x : E), u (-x) = u x
def ExistsContDiffBumpBase.u {E : Type u_1} [] [] (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
Instances For
theorem ExistsContDiffBumpBase.u_smooth (E : Type u_1) [] [] :
ContDiff ExistsContDiffBumpBase.u
theorem ExistsContDiffBumpBase.u_continuous (E : Type u_1) [] [] :
Continuous ExistsContDiffBumpBase.u
theorem ExistsContDiffBumpBase.u_support (E : Type u_1) [] [] :
Function.support ExistsContDiffBumpBase.u =
theorem ExistsContDiffBumpBase.u_compact_support (E : Type u_1) [] [] :
HasCompactSupport ExistsContDiffBumpBase.u
theorem ExistsContDiffBumpBase.u_nonneg {E : Type u_1} [] [] (x : E) :
theorem ExistsContDiffBumpBase.u_le_one {E : Type u_1} [] [] (x : E) :
theorem ExistsContDiffBumpBase.u_neg {E : Type u_1} [] [] (x : E) :
theorem ExistsContDiffBumpBase.u_int_pos (E : Type u_1) [] [] [] [] :
0 < ∫ (x : E), MeasureTheory.Measure.addHaar
def ExistsContDiffBumpBase.w {E : Type u_1} [] [] [] [] (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
• = ((∫ (x : E), ∂MeasureTheory.Measure.addHaar) * )⁻¹
Instances For
theorem ExistsContDiffBumpBase.w_def {E : Type u_1} [] [] [] [] (D : ) :
= fun (x : E) => ((∫ (x : E), MeasureTheory.Measure.addHaar) * )⁻¹
theorem ExistsContDiffBumpBase.w_nonneg {E : Type u_1} [] [] [] [] (D : ) (x : E) :
theorem ExistsContDiffBumpBase.w_mul_φ_nonneg {E : Type u_1} [] [] [] [] (D : ) (x : E) (y : E) :
0
theorem ExistsContDiffBumpBase.w_integral (E : Type u_1) [] [] [] [] {D : } (Dpos : 0 < D) :
∫ (x : E), MeasureTheory.Measure.addHaar = 1
theorem ExistsContDiffBumpBase.w_support (E : Type u_1) [] [] [] [] {D : } (Dpos : 0 < D) :
theorem ExistsContDiffBumpBase.w_compact_support (E : Type u_1) [] [] [] [] {D : } (Dpos : 0 < D) :
def ExistsContDiffBumpBase.y {E : Type u_1} [] [] [] [] (D : ) :
E

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
Instances For
theorem ExistsContDiffBumpBase.y_neg {E : Type u_1} [] [] [] [] (D : ) (x : E) :
theorem ExistsContDiffBumpBase.y_eq_one_of_mem_closedBall {E : Type u_1} [] [] [] [] {D : } {x : E} (Dpos : 0 < D) (hx : x Metric.closedBall 0 (1 - D)) :
theorem ExistsContDiffBumpBase.y_eq_zero_of_not_mem_ball {E : Type u_1} [] [] [] [] {D : } {x : E} (Dpos : 0 < D) (hx : xMetric.ball 0 (1 + D)) :
theorem ExistsContDiffBumpBase.y_nonneg {E : Type u_1} [] [] [] [] (D : ) (x : E) :
theorem ExistsContDiffBumpBase.y_le_one {E : Type u_1} [] [] [] [] {D : } (x : E) (Dpos : 0 < D) :
theorem ExistsContDiffBumpBase.y_pos_of_mem_ball {E : Type u_1} [] [] [] [] {D : } {x : E} (Dpos : 0 < D) (D_lt_one : D < 1) (hx : x Metric.ball 0 (1 + D)) :
theorem ExistsContDiffBumpBase.y_smooth (E : Type u_1) [] [] [] [] :
ContDiffOn (Function.uncurry ExistsContDiffBumpBase.y) (Set.Ioo 0 1 ×ˢ Set.univ)
theorem ExistsContDiffBumpBase.y_support (E : Type u_1) [] [] [] [] {D : } (Dpos : 0 < D) (D_lt_one : D < 1) :
= Metric.ball 0 (1 + D)
@[instance 100]
Equations
• =