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.

theorem exists_smooth_tsupport_subset {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] {s : set E} {x : E} (hs : s ∈ nhds x) :

∃ (f : E → ℝ), tsupport f ⊆ s ∧ has_compact_support f ∧ cont_diff ℝ ⊤ 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 is_open.exists_smooth_support_eq {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] {s : set E} (hs : is_open s) :

∃ (f : E → ℝ), function.support f = s ∧ cont_diff ℝ ⊤ 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.

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

exists_cont_diff_bump_base.φ = (metric.closed_ball 0 1).indicator (λ (y : E), 1)

theorem exists_cont_diff_bump_base.u_exists (E : Type u_1) [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] :

∃ (u : E → ℝ), cont_diff ℝ ⊤ u ∧ (∀ (x : E), u x ∈ set.Icc 0 1) ∧ function.support u = metric.ball 0 1 ∧ ∀ (x : E), u (-x) = u x

noncomputable def exists_cont_diff_bump_base.u {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ 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

exists_cont_diff_bump_base.u x = classical.some _ x

theorem exists_cont_diff_bump_base.u_smooth (E : Type u_1) [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] :

cont_diff ℝ ⊤ exists_cont_diff_bump_base.u

theorem exists_cont_diff_bump_base.u_continuous (E : Type u_1) [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] :

continuous exists_cont_diff_bump_base.u

theorem exists_cont_diff_bump_base.u_support (E : Type u_1) [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] :

function.support exists_cont_diff_bump_base.u = metric.ball 0 1

theorem exists_cont_diff_bump_base.u_compact_support (E : Type u_1) [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] :

has_compact_support exists_cont_diff_bump_base.u

theorem exists_cont_diff_bump_base.u_nonneg {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] (x : E) :

0 ≤ exists_cont_diff_bump_base.u x

theorem exists_cont_diff_bump_base.u_le_one {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] (x : E) :

exists_cont_diff_bump_base.u x ≤ 1

theorem exists_cont_diff_bump_base.u_neg {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] (x : E) :

exists_cont_diff_bump_base.u (-x) = exists_cont_diff_bump_base.u x

theorem exists_cont_diff_bump_base.u_int_pos (E : Type u_1) [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] [measurable_space E] [borel_space E] :

0 < ∫ (x : E), exists_cont_diff_bump_base.u x ∂measure_theory.measure.add_haar

noncomputable def exists_cont_diff_bump_base.W {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] [measurable_space E] [borel_space 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

exists_cont_diff_bump_base.W D x = (∫ (x : E), exists_cont_diff_bump_base.u x ∂measure_theory.measure.add_haar * |D| ^ fdim E)⁻¹ • exists_cont_diff_bump_base.u (D⁻¹ • x)

theorem exists_cont_diff_bump_base.W_def {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] [measurable_space E] [borel_space E] (D : ℝ) :

exists_cont_diff_bump_base.W D = λ (x : E), (∫ (x : E), exists_cont_diff_bump_base.u x ∂measure_theory.measure.add_haar * |D| ^ fdim E)⁻¹ • exists_cont_diff_bump_base.u (D⁻¹ • x)

theorem exists_cont_diff_bump_base.W_nonneg {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] [measurable_space E] [borel_space E] (D : ℝ) (x : E) :

0 ≤ exists_cont_diff_bump_base.W D x

theorem exists_cont_diff_bump_base.W_mul_φ_nonneg {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] [measurable_space E] [borel_space E] (D : ℝ) (x y : E) :

0 ≤ exists_cont_diff_bump_base.W D y * exists_cont_diff_bump_base.φ (x - y)

theorem exists_cont_diff_bump_base.W_integral (E : Type u_1) [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] [measurable_space E] [borel_space E] {D : ℝ} (Dpos : 0 < D) :

∫ (x : E), exists_cont_diff_bump_base.W D x ∂measure_theory.measure.add_haar = 1

theorem exists_cont_diff_bump_base.W_support (E : Type u_1) [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] [measurable_space E] [borel_space E] {D : ℝ} (Dpos : 0 < D) :

function.support (exists_cont_diff_bump_base.W D) = metric.ball 0 D

theorem exists_cont_diff_bump_base.W_compact_support (E : Type u_1) [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] [measurable_space E] [borel_space E] {D : ℝ} (Dpos : 0 < D) :

has_compact_support (exists_cont_diff_bump_base.W D)

noncomputable def exists_cont_diff_bump_base.Y {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] [measurable_space E] [borel_space E] (D : ℝ) :

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

exists_cont_diff_bump_base.Y D = convolution (exists_cont_diff_bump_base.W D) exists_cont_diff_bump_base.φ (continuous_linear_map.lsmul ℝ ℝ) measure_theory.measure.add_haar

theorem exists_cont_diff_bump_base.Y_neg {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] [measurable_space E] [borel_space E] (D : ℝ) (x : E) :

exists_cont_diff_bump_base.Y D (-x) = exists_cont_diff_bump_base.Y D x

theorem exists_cont_diff_bump_base.Y_eq_one_of_mem_closed_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) (hx : x ∈ metric.closed_ball 0 (1 - D)) :

exists_cont_diff_bump_base.Y D x = 1

theorem exists_cont_diff_bump_base.Y_eq_zero_of_not_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) (hx : x ∉ metric.ball 0 (1 + D)) :

exists_cont_diff_bump_base.Y D x = 0

theorem exists_cont_diff_bump_base.Y_nonneg {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] [measurable_space E] [borel_space E] (D : ℝ) (x : E) :

0 ≤ exists_cont_diff_bump_base.Y D x

theorem exists_cont_diff_bump_base.Y_le_one {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) :

exists_cont_diff_bump_base.Y D x ≤ 1

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

0 < exists_cont_diff_bump_base.Y D x

theorem exists_cont_diff_bump_base.Y_smooth (E : Type u_1) [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] [measurable_space E] [borel_space E] :

cont_diff_on ℝ ⊤ (function.uncurry exists_cont_diff_bump_base.Y) (set.Ioo 0 1 ×ˢ set.univ)

theorem exists_cont_diff_bump_base.Y_support (E : Type u_1) [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] [measurable_space E] [borel_space E] {D : ℝ} (Dpos : 0 < D) (D_lt_one : D < 1) :

function.support (exists_cont_diff_bump_base.Y D) = metric.ball 0 (1 + D)

@[protected, instance]

def exists_cont_diff_bump_base.has_cont_diff_bump {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] :

has_cont_diff_bump E