Documentation

Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

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_contDiff_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_contDiff_tsupport_subset {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} {x : E} {n : ℕ∞} (hs : s ∈ nhds x) :

∃ (f : E → ℝ), tsupport f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ (↑n) 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.

@[deprecated exists_contDiff_tsupport_subset (since := "2025-12-17")]

theorem exists_smooth_tsupport_subset {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} {x : E} {n : ℕ∞} (hs : s ∈ nhds x) :

∃ (f : E → ℝ), tsupport f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ (↑n) f ∧ Set.range f ⊆ Set.Icc 0 1 ∧ f x = 1

Alias of exists_contDiff_tsupport_subset.

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_contDiff_support_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ∞} {s : Set E} (hs : IsOpen s) :

∃ (f : E → ℝ), Function.support f = s ∧ ContDiff ℝ (↑n) 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.

@[deprecated IsOpen.exists_contDiff_support_eq (since := "2025-12-17")]

theorem IsOpen.exists_smooth_support_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ∞} {s : Set E} (hs : IsOpen s) :

∃ (f : E → ℝ), Function.support f = s ∧ ContDiff ℝ (↑n) f ∧ Set.range f ⊆ Set.Icc 0 1

Alias of IsOpen.exists_contDiff_support_eq.

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

Instances For

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

Instances For

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] :

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

Instances For

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

Instances For

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

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