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} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} {x : E} (hs : s ∈ nhds x) : ∃ (f : E → ℝ), tsupport f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ (↑⊤) f ∧ Set.range f ⊆ 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} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} (hs : IsOpen s) : ∃ (f : E → ℝ), Function.support f = s ∧ ContDiff ℝ (↑⊤) f ∧ Set.range f ⊆ 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} [NormedAddCommGroup E] : 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.φ = (Metric.closedBall 0 1).indicator fun (x : E) => 1

theorem ExistsContDiffBumpBase.u_exists (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] : ∃ (u : E → ℝ), ContDiff ℝ (↑⊤) u ∧ (∀ (x : E), u x ∈ Set.Icc 0 1) ∧ Function.support u = Metric.ball 0 1 ∧ ∀ (x : E), u (-x) = u x

def ExistsContDiffBumpBase.u {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ 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

• ExistsContDiffBumpBase.u x = Classical.choose ⋯ x

theorem ExistsContDiffBumpBase.u_smooth (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] : ContDiff ℝ (↑⊤) u

theorem ExistsContDiffBumpBase.u_continuous (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] : Continuous u

theorem ExistsContDiffBumpBase.u_support (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] : Function.support u = Metric.ball 0 1

theorem ExistsContDiffBumpBase.u_compact_support (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] : HasCompactSupport u

theorem ExistsContDiffBumpBase.u_nonneg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (x : E) : 0 ≤ u x

theorem ExistsContDiffBumpBase.u_le_one {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (x : E) : u x ≤ 1

theorem ExistsContDiffBumpBase.u_neg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (x : E) : u (-x) = u x

theorem ExistsContDiffBumpBase.u_int_pos (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] : 0 < ∫ (x : E), u x ∂MeasureTheory.Measure.addHaar

def ExistsContDiffBumpBase.w {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace 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

• ExistsContDiffBumpBase.w D x = ((∫ (x : E), ExistsContDiffBumpBase.u x ∂MeasureTheory.Measure.addHaar) * |D| ^ Module.finrank ℝ E)⁻¹ • ExistsContDiffBumpBase.u (D⁻¹ • x)

theorem ExistsContDiffBumpBase.w_def {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (D : ℝ) : w D = fun (x : E) => ((∫ (x : E), u x ∂MeasureTheory.Measure.addHaar) * |D| ^ Module.finrank ℝ E)⁻¹ • u (D⁻¹ • x)

theorem ExistsContDiffBumpBase.w_nonneg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (D : ℝ) (x : E) : 0 ≤ w D x

theorem ExistsContDiffBumpBase.w_mul_φ_nonneg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (D : ℝ) (x y : E) : 0 ≤ w D y * φ (x - y)

theorem ExistsContDiffBumpBase.w_integral (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {D : ℝ} (Dpos : 0 < D) : ∫ (x : E), w D x ∂MeasureTheory.Measure.addHaar = 1

theorem ExistsContDiffBumpBase.w_support (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {D : ℝ} (Dpos : 0 < D) : Function.support (w D) = Metric.ball 0 D

theorem ExistsContDiffBumpBase.w_compact_support (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {D : ℝ} (Dpos : 0 < D) : HasCompactSupport (w D)

def ExistsContDiffBumpBase.y {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (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

• ExistsContDiffBumpBase.y D = MeasureTheory.convolution (ExistsContDiffBumpBase.w D) ExistsContDiffBumpBase.φ (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.Measure.addHaar

theorem ExistsContDiffBumpBase.y_neg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (D : ℝ) (x : E) : y D (-x) = y D x

theorem ExistsContDiffBumpBase.y_eq_one_of_mem_closedBall {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {D : ℝ} {x : E} (Dpos : 0 < D) (hx : x ∈ Metric.closedBall 0 (1 - D)) : y D x = 1

theorem ExistsContDiffBumpBase.y_eq_zero_of_notMem_ball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {D : ℝ} {x : E} (Dpos : 0 < D) (hx : x ∉ Metric.ball 0 (1 + D)) : y D x = 0

@[deprecated ExistsContDiffBumpBase.y_eq_zero_of_notMem_ball (since := "2025-05-23")]

theorem ExistsContDiffBumpBase.y_eq_zero_of_not_mem_ball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {D : ℝ} {x : E} (Dpos : 0 < D) (hx : x ∉ Metric.ball 0 (1 + D)) : y D x = 0

Alias of ExistsContDiffBumpBase.y_eq_zero_of_notMem_ball.

theorem ExistsContDiffBumpBase.y_nonneg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (D : ℝ) (x : E) : 0 ≤ y D x

theorem ExistsContDiffBumpBase.y_le_one {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {D : ℝ} (x : E) (Dpos : 0 < D) : y D x ≤ 1

theorem ExistsContDiffBumpBase.y_pos_of_mem_ball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {D : ℝ} {x : E} (Dpos : 0 < D) (D_lt_one : D < 1) (hx : x ∈ Metric.ball 0 (1 + D)) : 0 < y D x

theorem ExistsContDiffBumpBase.y_smooth (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] : ContDiffOn ℝ (↑⊤) (Function.uncurry y) (Set.Ioo 0 1 ×ˢ Set.univ)

theorem ExistsContDiffBumpBase.y_support (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {D : ℝ} (Dpos : 0 < D) (D_lt_one : D < 1) : Function.support (y D) = Metric.ball 0 (1 + D)

@[instance 100]

instance ExistsContDiffBumpBase.instHasContDiffBumpOfFiniteDimensionalReal {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] : HasContDiffBump E