mathlib documentation

analysis.calculus.specific_functions

Infinitely smooth bump function #

In this file we construct several infinitely smooth functions with properties that an analytic function cannot have:

exp_neg_inv_glue is equal to zero for x ≤ 0 and is strictly positive otherwise; it is given by x ↦ exp (-1/x) for x > 0;
real.smooth_transition is equal to zero for x ≤ 0 and is equal to one for x ≥ 1; it is given by exp_neg_inv_glue x / (exp_neg_inv_glue x + exp_neg_inv_glue (1 - x));
f : cont_diff_bump_of_inner c, where c is a point in an inner product space, is a bundled smooth function such that
- f is equal to 1 in metric.closed_ball c f.r;
- support f = metric.ball c f.R;
- 0 ≤ f x ≤ 1 for all x.
The structure cont_diff_bump_of_inner contains the data required to construct the function: real numbers r, R, and proofs of 0 < r < R. The function itself is available through coe_fn.
If f : cont_diff_bump_of_inner c and μ is a measure on the domain of f, then f.normed μ is a smooth bump function with integral 1 w.r.t. μ.
f : cont_diff_bump c, where c is a point in a finite dimensional real vector space, is a bundled smooth function such that
- f is equal to 1 in euclidean.closed_ball c f.r;
- support f = euclidean.ball c f.R;
- 0 ≤ f x ≤ 1 for all x.
The structure cont_diff_bump contains the data required to construct the function: real numbers r, R, and proofs of 0 < r < R. The function itself is available through coe_fn.

noncomputable def exp_neg_inv_glue (x : ℝ) :

exp_neg_inv_glue is the real function given by x ↦ exp (-1/x) for x > 0 and 0 for x ≤ 0. It is a basic building block to construct smooth partitions of unity. Its main property is that it vanishes for x ≤ 0, it is positive for x > 0, and the junction between the two behaviors is flat enough to retain smoothness. The fact that this function is C^∞ is proved in exp_neg_inv_glue.smooth.

Equations

exp_neg_inv_glue x = ite (x ≤ 0) 0 (real.exp (-x⁻¹))

noncomputable def exp_neg_inv_glue.P_aux :

ℕ → polynomial ℝ

Our goal is to prove that exp_neg_inv_glue is C^∞. For this, we compute its successive derivatives for x > 0. The n-th derivative is of the form P_aux n (x) exp(-1/x) / x^(2 n), where P_aux n is computed inductively.

Equations

exp_neg_inv_glue.P_aux (n + 1) = polynomial.X ^ 2 * ⇑polynomial.derivative (exp_neg_inv_glue.P_aux n) + (1 - ⇑polynomial.C ↑(2 * n) * polynomial.X) * exp_neg_inv_glue.P_aux n
exp_neg_inv_glue.P_aux 0 = 1

noncomputable def exp_neg_inv_glue.f_aux (n : ℕ) (x : ℝ) :

Formula for the n-th derivative of exp_neg_inv_glue, as an auxiliary function f_aux.

Equations

exp_neg_inv_glue.f_aux n x = ite (x ≤ 0) 0 (polynomial.eval x (exp_neg_inv_glue.P_aux n) * real.exp (-x⁻¹) / x ^ (2 * n))

theorem exp_neg_inv_glue.f_aux_zero_eq :

exp_neg_inv_glue.f_aux 0 = exp_neg_inv_glue

The 0-th auxiliary function f_aux 0 coincides with exp_neg_inv_glue, by definition.

theorem exp_neg_inv_glue.f_aux_deriv (n : ℕ) (x : ℝ) (hx : x ≠ 0) :

has_deriv_at (λ (x : ℝ), polynomial.eval x (exp_neg_inv_glue.P_aux n) * real.exp (-x⁻¹) / x ^ (2 * n)) (polynomial.eval x (exp_neg_inv_glue.P_aux (n + 1)) * real.exp (-x⁻¹) / x ^ (2 * (n + 1))) x

For positive values, the derivative of the n-th auxiliary function f_aux n (given in this statement in unfolded form) is the n+1-th auxiliary function, since the polynomial P_aux (n+1) was chosen precisely to ensure this.

theorem exp_neg_inv_glue.f_aux_deriv_pos (n : ℕ) (x : ℝ) (hx : 0 < x) :

has_deriv_at (exp_neg_inv_glue.f_aux n) (polynomial.eval x (exp_neg_inv_glue.P_aux (n + 1)) * real.exp (-x⁻¹) / x ^ (2 * (n + 1))) x

For positive values, the derivative of the n-th auxiliary function f_aux n is the n+1-th auxiliary function.

theorem exp_neg_inv_glue.f_aux_limit (n : ℕ) :

filter.tendsto (λ (x : ℝ), polynomial.eval x (exp_neg_inv_glue.P_aux n) * real.exp (-x⁻¹) / x ^ (2 * n)) (nhds_within 0 (set.Ioi 0)) (nhds 0)

To get differentiability at 0 of the auxiliary functions, we need to know that their limit is 0, to be able to apply general differentiability extension theorems. This limit is checked in this lemma.

theorem exp_neg_inv_glue.f_aux_deriv_zero (n : ℕ) :

has_deriv_at (exp_neg_inv_glue.f_aux n) 0 0

Deduce from the limiting behavior at 0 of its derivative and general differentiability extension theorems that the auxiliary function f_aux n is differentiable at 0, with derivative 0.

theorem exp_neg_inv_glue.f_aux_has_deriv_at (n : ℕ) (x : ℝ) :

has_deriv_at (exp_neg_inv_glue.f_aux n) (exp_neg_inv_glue.f_aux (n + 1) x) x

At every point, the auxiliary function f_aux n has a derivative which is equal to f_aux (n+1).

theorem exp_neg_inv_glue.f_aux_iterated_deriv (n : ℕ) :

iterated_deriv n (exp_neg_inv_glue.f_aux 0) = exp_neg_inv_glue.f_aux n

The successive derivatives of the auxiliary function f_aux 0 are the functions f_aux n, by induction.

@[protected]

theorem exp_neg_inv_glue.cont_diff {n : ℕ∞} :

cont_diff ℝ n exp_neg_inv_glue

The function exp_neg_inv_glue is smooth.

theorem exp_neg_inv_glue.zero_of_nonpos {x : ℝ} (hx : x ≤ 0) :

exp_neg_inv_glue x = 0

The function exp_neg_inv_glue vanishes on (-∞, 0].

theorem exp_neg_inv_glue.pos_of_pos {x : ℝ} (hx : 0 < x) :

0 < exp_neg_inv_glue x

The function exp_neg_inv_glue is positive on (0, +∞).

theorem exp_neg_inv_glue.nonneg (x : ℝ) :

0 ≤ exp_neg_inv_glue x

The function exp_neg_inv_glue` is nonnegative.

noncomputable def real.smooth_transition (x : ℝ) :

An infinitely smooth function f : ℝ → ℝ such that f x = 0 for x ≤ 0, f x = 1 for 1 ≤ x, and 0 < f x < 1 for 0 < x < 1.

Equations

x.smooth_transition = exp_neg_inv_glue x / (exp_neg_inv_glue x + exp_neg_inv_glue (1 - x))

theorem real.smooth_transition.pos_denom (x : ℝ) :

0 < exp_neg_inv_glue x + exp_neg_inv_glue (1 - x)

theorem real.smooth_transition.one_of_one_le {x : ℝ} (h : 1 ≤ x) :

x.smooth_transition = 1

theorem real.smooth_transition.zero_of_nonpos {x : ℝ} (h : x ≤ 0) :

x.smooth_transition = 0

@[protected, simp]

theorem real.smooth_transition.zero :

0.smooth_transition = 0

@[protected, simp]

theorem real.smooth_transition.one :

1.smooth_transition = 1

theorem real.smooth_transition.le_one (x : ℝ) :

x.smooth_transition ≤ 1

theorem real.smooth_transition.nonneg (x : ℝ) :

0 ≤ x.smooth_transition

theorem real.smooth_transition.lt_one_of_lt_one {x : ℝ} (h : x < 1) :

x.smooth_transition < 1

theorem real.smooth_transition.pos_of_pos {x : ℝ} (h : 0 < x) :

0 < x.smooth_transition

@[protected]

theorem real.smooth_transition.cont_diff {n : ℕ∞} :

cont_diff ℝ n real.smooth_transition

@[protected]

theorem real.smooth_transition.cont_diff_at {x : ℝ} {n : ℕ∞} :

cont_diff_at ℝ n real.smooth_transition x

@[protected]

theorem real.smooth_transition.continuous :

continuous real.smooth_transition

structure cont_diff_bump_of_inner {E : Type u_1} (c : E) :

Type

r : ℝ
R : ℝ
r_pos : 0 < self.r
r_lt_R : self.r < self.R

f : cont_diff_bump_of_inner c, where c is a point in an inner product space, is a bundled smooth function such that

f is equal to 1 in metric.closed_ball c f.r;
support f = metric.ball c f.R;
0 ≤ f x ≤ 1 for all x.

The structure cont_diff_bump_of_inner contains the data required to construct the function: real numbers r, R, and proofs of 0 < r < R. The function itself is available through coe_fn.

Instances for cont_diff_bump_of_inner

theorem cont_diff_bump_of_inner.R_pos {E : Type u_1} {c : E} (f : cont_diff_bump_of_inner c) :

0 < f.R

@[protected, instance]

def cont_diff_bump_of_inner.inhabited {E : Type u_1} (c : E) :

inhabited (cont_diff_bump_of_inner c)

Equations

cont_diff_bump_of_inner.inhabited c = {default := {r := 1, R := 2, r_pos := _, r_lt_R := _}}

noncomputable def cont_diff_bump_of_inner.to_fun {E : Type u_1} [inner_product_space ℝ E] {c : E} (f : cont_diff_bump_of_inner c) :

E → ℝ

The function defined by f : cont_diff_bump_of_inner c. Use automatic coercion to function instead.

Equations

f.to_fun = λ (x : E), ((f.R - has_dist.dist x c) / (f.R - f.r)).smooth_transition

@[protected, instance]

noncomputable def cont_diff_bump_of_inner.has_coe_to_fun {E : Type u_1} [inner_product_space ℝ E] {c : E} :

has_coe_to_fun (cont_diff_bump_of_inner c) (λ (_x : cont_diff_bump_of_inner c), E → ℝ)

Equations

cont_diff_bump_of_inner.has_coe_to_fun = {coe := cont_diff_bump_of_inner.to_fun c}

@[protected]

theorem cont_diff_bump_of_inner.def {E : Type u_1} [inner_product_space ℝ E] {c : E} (f : cont_diff_bump_of_inner c) (x : E) :

⇑f x = ((f.R - has_dist.dist x c) / (f.R - f.r)).smooth_transition

@[protected]

theorem cont_diff_bump_of_inner.sub {E : Type u_1} [inner_product_space ℝ E] {c : E} (f : cont_diff_bump_of_inner c) (x : E) :

⇑f (c - x) = ⇑f (c + x)

@[protected]

theorem cont_diff_bump_of_inner.neg {E : Type u_1} [inner_product_space ℝ E] (f : cont_diff_bump_of_inner 0) (x : E) :

⇑f (-x) = ⇑f x

theorem cont_diff_bump_of_inner.one_of_mem_closed_ball {E : Type u_1} [inner_product_space ℝ E] {c : E} (f : cont_diff_bump_of_inner c) {x : E} (hx : x ∈ metric.closed_ball c f.r) :

⇑f x = 1

theorem cont_diff_bump_of_inner.nonneg {E : Type u_1} [inner_product_space ℝ E] {c : E} (f : cont_diff_bump_of_inner c) {x : E} :

0 ≤ ⇑f x

theorem cont_diff_bump_of_inner.nonneg' {E : Type u_1} [inner_product_space ℝ E] {c : E} (f : cont_diff_bump_of_inner c) (x : E) :

0 ≤ ⇑f x

A version of cont_diff_bump_of_inner.nonneg with x explicit

theorem cont_diff_bump_of_inner.le_one {E : Type u_1} [inner_product_space ℝ E] {c : E} (f : cont_diff_bump_of_inner c) {x : E} :

⇑f x ≤ 1

theorem cont_diff_bump_of_inner.pos_of_mem_ball {E : Type u_1} [inner_product_space ℝ E] {c : E} (f : cont_diff_bump_of_inner c) {x : E} (hx : x ∈ metric.ball c f.R) :

0 < ⇑f x

theorem cont_diff_bump_of_inner.lt_one_of_lt_dist {E : Type u_1} [inner_product_space ℝ E] {c : E} (f : cont_diff_bump_of_inner c) {x : E} (h : f.r < has_dist.dist x c) :

⇑f x < 1

theorem cont_diff_bump_of_inner.zero_of_le_dist {E : Type u_1} [inner_product_space ℝ E] {c : E} (f : cont_diff_bump_of_inner c) {x : E} (hx : f.R ≤ has_dist.dist x c) :

⇑f x = 0

theorem cont_diff_bump_of_inner.support_eq {E : Type u_1} [inner_product_space ℝ E] {c : E} (f : cont_diff_bump_of_inner c) :

function.support ⇑f = metric.ball c f.R

theorem cont_diff_bump_of_inner.tsupport_eq {E : Type u_1} [inner_product_space ℝ E] {c : E} (f : cont_diff_bump_of_inner c) :

tsupport ⇑f = metric.closed_ball c f.R

@[protected]

theorem cont_diff_bump_of_inner.has_compact_support {E : Type u_1} [inner_product_space ℝ E] {c : E} (f : cont_diff_bump_of_inner c) [finite_dimensional ℝ E] :

has_compact_support ⇑f

theorem cont_diff_bump_of_inner.eventually_eq_one_of_mem_ball {E : Type u_1} [inner_product_space ℝ E] {c : E} (f : cont_diff_bump_of_inner c) {x : E} (h : x ∈ metric.ball c f.r) :

⇑f =ᶠ[nhds x] 1

theorem cont_diff_bump_of_inner.eventually_eq_one {E : Type u_1} [inner_product_space ℝ E] {c : E} (f : cont_diff_bump_of_inner c) :

⇑f =ᶠ[nhds c] 1

@[protected]

theorem cont_diff_at.cont_diff_bump {E : Type u_1} {X : Type u_2} [inner_product_space ℝ E] [normed_add_comm_group X] [normed_space ℝ X] {n : ℕ∞} {c g : X → E} {f : Π (x : X), cont_diff_bump_of_inner (c x)} {x : X} (hc : cont_diff_at ℝ n c x) (hr : cont_diff_at ℝ n (λ (x : X), (f x).r) x) (hR : cont_diff_at ℝ n (λ (x : X), (f x).R) x) (hg : cont_diff_at ℝ n g x) :

cont_diff_at ℝ n (λ (x : X), ⇑(f x) (g x)) x

cont_diff_bump is 𝒞ⁿ in all its arguments.

theorem cont_diff.cont_diff_bump {E : Type u_1} {X : Type u_2} [inner_product_space ℝ E] [normed_add_comm_group X] [normed_space ℝ X] {n : ℕ∞} {c g : X → E} {f : Π (x : X), cont_diff_bump_of_inner (c x)} (hc : cont_diff ℝ n c) (hr : cont_diff ℝ n (λ (x : X), (f x).r)) (hR : cont_diff ℝ n (λ (x : X), (f x).R)) (hg : cont_diff ℝ n g) :

cont_diff ℝ n (λ (x : X), ⇑(f x) (g x))

@[protected]

theorem cont_diff_bump_of_inner.cont_diff {E : Type u_1} [inner_product_space ℝ E] {c : E} (f : cont_diff_bump_of_inner c) {n : ℕ∞} :

cont_diff ℝ n ⇑f

@[protected]

theorem cont_diff_bump_of_inner.cont_diff_at {E : Type u_1} [inner_product_space ℝ E] {c : E} (f : cont_diff_bump_of_inner c) {x : E} {n : ℕ∞} :

cont_diff_at ℝ n ⇑f x

@[protected]

theorem cont_diff_bump_of_inner.cont_diff_within_at {E : Type u_1} [inner_product_space ℝ E] {c : E} (f : cont_diff_bump_of_inner c) {x : E} {n : ℕ∞} {s : set E} :

cont_diff_within_at ℝ n ⇑f s x

@[protected]

theorem cont_diff_bump_of_inner.continuous {E : Type u_1} [inner_product_space ℝ E] {c : E} (f : cont_diff_bump_of_inner c) :

continuous ⇑f

@[protected]

noncomputable def cont_diff_bump_of_inner.normed {E : Type u_1} [inner_product_space ℝ E] {c : E} (f : cont_diff_bump_of_inner c) [measurable_space E] (μ : measure_theory.measure E) :

E → ℝ

A bump function normed so that ∫ x, f.normed μ x ∂μ = 1.

Equations

f.normed μ = λ (x : E), ⇑f x / ∫ (x : E), ⇑f x ∂μ

theorem cont_diff_bump_of_inner.normed_def {E : Type u_1} [inner_product_space ℝ E] {c : E} (f : cont_diff_bump_of_inner c) [measurable_space E] {μ : measure_theory.measure E} (x : E) :

f.normed μ x = ⇑f x / ∫ (x : E), ⇑f x ∂μ

theorem cont_diff_bump_of_inner.nonneg_normed {E : Type u_1} [inner_product_space ℝ E] {c : E} (f : cont_diff_bump_of_inner c) [measurable_space E] {μ : measure_theory.measure E} (x : E) :

0 ≤ f.normed μ x

theorem cont_diff_bump_of_inner.cont_diff_normed {E : Type u_1} [inner_product_space ℝ E] {c : E} (f : cont_diff_bump_of_inner c) [measurable_space E] {μ : measure_theory.measure E} {n : ℕ∞} :

cont_diff ℝ n (f.normed μ)

theorem cont_diff_bump_of_inner.continuous_normed {E : Type u_1} [inner_product_space ℝ E] {c : E} (f : cont_diff_bump_of_inner c) [measurable_space E] {μ : measure_theory.measure E} :

continuous (f.normed μ)

theorem cont_diff_bump_of_inner.normed_sub {E : Type u_1} [inner_product_space ℝ E] {c : E} (f : cont_diff_bump_of_inner c) [measurable_space E] {μ : measure_theory.measure E} (x : E) :

f.normed μ (c - x) = f.normed μ (c + x)

theorem cont_diff_bump_of_inner.normed_neg {E : Type u_1} [inner_product_space ℝ E] [measurable_space E] {μ : measure_theory.measure E} (f : cont_diff_bump_of_inner 0) (x : E) :

f.normed μ (-x) = f.normed μ x

@[protected]

theorem cont_diff_bump_of_inner.integrable {E : Type u_1} [inner_product_space ℝ E] {c : E} (f : cont_diff_bump_of_inner c) [measurable_space E] {μ : measure_theory.measure E} [borel_space E] [finite_dimensional ℝ E] [measure_theory.is_locally_finite_measure μ] :

measure_theory.integrable ⇑f μ

@[protected]

theorem cont_diff_bump_of_inner.integrable_normed {E : Type u_1} [inner_product_space ℝ E] {c : E} (f : cont_diff_bump_of_inner c) [measurable_space E] {μ : measure_theory.measure E} [borel_space E] [finite_dimensional ℝ E] [measure_theory.is_locally_finite_measure μ] :

measure_theory.integrable (f.normed μ) μ

theorem cont_diff_bump_of_inner.integral_pos {E : Type u_1} [inner_product_space ℝ E] {c : E} (f : cont_diff_bump_of_inner c) [measurable_space E] {μ : measure_theory.measure E} [borel_space E] [finite_dimensional ℝ E] [measure_theory.is_locally_finite_measure μ] [μ.is_open_pos_measure] :

0 < ∫ (x : E), ⇑f x ∂μ

theorem cont_diff_bump_of_inner.integral_normed {E : Type u_1} [inner_product_space ℝ E] {c : E} (f : cont_diff_bump_of_inner c) [measurable_space E] {μ : measure_theory.measure E} [borel_space E] [finite_dimensional ℝ E] [measure_theory.is_locally_finite_measure μ] [μ.is_open_pos_measure] :

∫ (x : E), f.normed μ x ∂μ = 1

theorem cont_diff_bump_of_inner.support_normed_eq {E : Type u_1} [inner_product_space ℝ E] {c : E} (f : cont_diff_bump_of_inner c) [measurable_space E] {μ : measure_theory.measure E} [borel_space E] [finite_dimensional ℝ E] [measure_theory.is_locally_finite_measure μ] [μ.is_open_pos_measure] :

function.support (f.normed μ) = metric.ball c f.R

theorem cont_diff_bump_of_inner.tsupport_normed_eq {E : Type u_1} [inner_product_space ℝ E] {c : E} (f : cont_diff_bump_of_inner c) [measurable_space E] {μ : measure_theory.measure E} [borel_space E] [finite_dimensional ℝ E] [measure_theory.is_locally_finite_measure μ] [μ.is_open_pos_measure] :

tsupport (f.normed μ) = metric.closed_ball c f.R

theorem cont_diff_bump_of_inner.has_compact_support_normed {E : Type u_1} [inner_product_space ℝ E] {c : E} (f : cont_diff_bump_of_inner c) [measurable_space E] {μ : measure_theory.measure E} [borel_space E] [finite_dimensional ℝ E] [measure_theory.is_locally_finite_measure μ] [μ.is_open_pos_measure] :

has_compact_support (f.normed μ)

theorem cont_diff_bump_of_inner.integral_normed_smul {E : Type u_1} {X : Type u_2} [inner_product_space ℝ E] [normed_add_comm_group X] [normed_space ℝ X] {c : E} (f : cont_diff_bump_of_inner c) [measurable_space E] (μ : measure_theory.measure E) [borel_space E] [finite_dimensional ℝ E] [measure_theory.is_locally_finite_measure μ] [μ.is_open_pos_measure] (z : X) [complete_space X] :

∫ (x : E), f.normed μ x • z ∂μ = z

structure cont_diff_bump {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] (c : E) :

Type

to_cont_diff_bump_of_inner : cont_diff_bump_of_inner (⇑to_euclidean c)

f : cont_diff_bump c, where c is a point in a finite dimensional real vector space, is a bundled smooth function such that

f is equal to 1 in euclidean.closed_ball c f.r;
support f = euclidean.ball c f.R;
0 ≤ f x ≤ 1 for all x.

The structure cont_diff_bump contains the data required to construct the function: real numbers r, R, and proofs of 0 < r < R. The function itself is available through coe_fn.

Instances for cont_diff_bump

noncomputable def cont_diff_bump.to_fun {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] {c : E} (f : cont_diff_bump c) :

E → ℝ

The function defined by f : cont_diff_bump c. Use automatic coercion to function instead.

Equations

f.to_fun = ⇑(f.to_cont_diff_bump_of_inner) ∘ ⇑to_euclidean

@[protected, instance]

noncomputable def cont_diff_bump.has_coe_to_fun {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] {c : E} :

has_coe_to_fun (cont_diff_bump c) (λ (_x : cont_diff_bump c), E → ℝ)

Equations

cont_diff_bump.has_coe_to_fun = {coe := cont_diff_bump.to_fun c}

@[protected, instance]

noncomputable def cont_diff_bump.inhabited {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] (c : E) :

inhabited (cont_diff_bump c)

Equations

cont_diff_bump.inhabited c = {default := {to_cont_diff_bump_of_inner := inhabited.default (cont_diff_bump_of_inner.inhabited (⇑to_euclidean c))}}

theorem cont_diff_bump.R_pos {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] {c : E} (f : cont_diff_bump c) :

0 < f.to_cont_diff_bump_of_inner.R

theorem cont_diff_bump.coe_eq_comp {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] {c : E} (f : cont_diff_bump c) :

⇑f = ⇑(f.to_cont_diff_bump_of_inner) ∘ ⇑to_euclidean

theorem cont_diff_bump.one_of_mem_closed_ball {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] {c x : E} (f : cont_diff_bump c) (hx : x ∈ euclidean.closed_ball c f.to_cont_diff_bump_of_inner.r) :

⇑f x = 1

theorem cont_diff_bump.nonneg {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] {c x : E} (f : cont_diff_bump c) :

0 ≤ ⇑f x

theorem cont_diff_bump.le_one {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] {c x : E} (f : cont_diff_bump c) :

⇑f x ≤ 1

theorem cont_diff_bump.pos_of_mem_ball {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] {c x : E} (f : cont_diff_bump c) (hx : x ∈ euclidean.ball c f.to_cont_diff_bump_of_inner.R) :

0 < ⇑f x

theorem cont_diff_bump.lt_one_of_lt_dist {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] {c x : E} (f : cont_diff_bump c) (h : f.to_cont_diff_bump_of_inner.r < euclidean.dist x c) :

⇑f x < 1

theorem cont_diff_bump.zero_of_le_dist {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] {c x : E} (f : cont_diff_bump c) (hx : f.to_cont_diff_bump_of_inner.R ≤ euclidean.dist x c) :

⇑f x = 0

theorem cont_diff_bump.support_eq {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] {c : E} (f : cont_diff_bump c) :

function.support ⇑f = euclidean.ball c f.to_cont_diff_bump_of_inner.R

theorem cont_diff_bump.tsupport_eq {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] {c : E} (f : cont_diff_bump c) :

tsupport ⇑f = euclidean.closed_ball c f.to_cont_diff_bump_of_inner.R

@[protected]

theorem cont_diff_bump.has_compact_support {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] {c : E} (f : cont_diff_bump c) :

has_compact_support ⇑f

theorem cont_diff_bump.eventually_eq_one_of_mem_ball {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] {c x : E} (f : cont_diff_bump c) (h : x ∈ euclidean.ball c f.to_cont_diff_bump_of_inner.r) :

⇑f =ᶠ[nhds x] 1

theorem cont_diff_bump.eventually_eq_one {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] {c : E} (f : cont_diff_bump c) :

⇑f =ᶠ[nhds c] 1

@[protected]

theorem cont_diff_bump.cont_diff {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] {c : E} (f : cont_diff_bump c) {n : ℕ∞} :

cont_diff ℝ n ⇑f

@[protected]

theorem cont_diff_bump.cont_diff_at {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] {c x : E} (f : cont_diff_bump c) {n : ℕ∞} :

cont_diff_at ℝ n ⇑f x

@[protected]

theorem cont_diff_bump.cont_diff_within_at {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] {c x : E} (f : cont_diff_bump c) {s : set E} {n : ℕ∞} :

cont_diff_within_at ℝ n ⇑f s x

theorem cont_diff_bump.exists_tsupport_subset {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] {c : E} {s : set E} (hs : s ∈ nhds c) :

∃ (f : cont_diff_bump c), tsupport ⇑f ⊆ s

theorem cont_diff_bump.exists_closure_subset {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] {c : E} {R : ℝ} (hR : 0 < R) {s : set E} (hs : is_closed s) (hsR : s ⊆ euclidean.ball c R) :

∃ (f : cont_diff_bump c), f.to_cont_diff_bump_of_inner.R = R ∧ s ⊆ euclidean.ball c f.to_cont_diff_bump_of_inner.r

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

∃ (f : E → ℝ), f =ᶠ[nhds x] 1 ∧ (∀ (y : E), f y ∈ set.Icc 0 1) ∧ cont_diff ℝ ⊤ f ∧ has_compact_support f ∧ tsupport f ⊆ s

If E is a finite dimensional normed space over ℝ, then for any point x : E and its neighborhood s there exists an infinitely smooth function with the following properties:

f y = 1 in a neighborhood of x;
f y = 0 outside of s;
moreover, tsupport f ⊆ s and f has compact support;
f y ∈ [0, 1] for all y.

This lemma is a simple wrapper around lemmas about bundled smooth bump functions, see cont_diff_bump.