mathlib3 documentation

analysis.calculus.bump_function_inner

Infinitely smooth bump function #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 c, where c is a point in a real vector 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 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 c and μ is a measure on the domain of f, then f.normed μ is a smooth bump function with integral 1 w.r.t. μ.

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 (rexp (-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) * rexp (-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) * rexp (-x⁻¹) / x ^ (2 * n)) (polynomial.eval x (exp_neg_inv_glue.P_aux (n + 1)) * rexp (-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)) * rexp (-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) * rexp (-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

@[protected, simp]

theorem real.smooth_transition.proj_Icc {x : ℝ} :

↑(set.proj_Icc 0 1 zero_le_one x).smooth_transition = x.smooth_transition

Since real.smooth_transition is constant on $(-∞, 0]$ and $[1, ∞)$, applying it to the projection of x : ℝ to $[0, 1]$ gives the same result as applying it to x.

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

@[protected]

theorem real.smooth_transition.continuous_at {x : ℝ} :

continuous_at real.smooth_transition x

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

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

f : cont_diff_bump c, where c is a point in a normed vector 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 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 when the space is nice enough, i.e., satisfies the has_cont_diff_bump typeclass.

Instances for cont_diff_bump

@[nolint]

structure cont_diff_bump_base (E : Type u_3) [normed_add_comm_group E] [normed_space ℝ E] :

Type u_3

to_fun : ℝ → E → ℝ
mem_Icc : ∀ (R : ℝ) (x : E), self.to_fun R x ∈ set.Icc 0 1
symmetric : ∀ (R : ℝ) (x : E), self.to_fun R (-x) = self.to_fun R x
smooth : cont_diff_on ℝ ⊤ (function.uncurry self.to_fun) (set.Ioi 1 ×ˢ set.univ)
eq_one : ∀ (R : ℝ), 1 < R → ∀ (x : E), ‖x‖ ≤ 1 → self.to_fun R x = 1
support : ∀ (R : ℝ), 1 < R → function.support (self.to_fun R) = metric.ball 0 R

The base function from which one will construct a family of bump functions. One could add more properties if they are useful and satisfied in the examples of inner product spaces and finite dimensional vector spaces, notably derivative norm control in terms of R - 1.

Instances for cont_diff_bump_base

cont_diff_bump_base.has_sizeof_inst

@[class]

structure has_cont_diff_bump (E : Type u_3) [normed_add_comm_group E] [normed_space ℝ E] :

Prop

out : nonempty (cont_diff_bump_base E)

A class registering that a real vector space admits bump functions. This will be instantiated first for inner product spaces, and then for finite-dimensional normed spaces. We use a specific class instead of nonempty (cont_diff_bump_base E) for performance reasons.

Instances of this typeclass

noncomputable def some_cont_diff_bump_base (E : Type u_1) [normed_add_comm_group E] [normed_space ℝ E] [hb : has_cont_diff_bump E] :

cont_diff_bump_base E

In a space with C^∞ bump functions, register some function that will be used as a basis to construct bump functions of arbitrary size around any point.

Equations

some_cont_diff_bump_base E = has_cont_diff_bump.out.some

@[protected, instance]

def has_cont_diff_bump_of_inner_product_space (E : Type u_1) [normed_add_comm_group E] [inner_product_space ℝ E] :

has_cont_diff_bump E

Any inner product space has smooth bump functions.

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

0 < f.R

theorem cont_diff_bump.one_lt_R_div_r {E : Type u_1} {c : E} (f : cont_diff_bump c) :

1 < f.R / f.r

@[protected, instance]

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

inhabited (cont_diff_bump c)

Equations

cont_diff_bump.inhabited c = {default := {r := 1, R := 2, r_pos := cont_diff_bump.inhabited._proof_1, r_lt_R := cont_diff_bump.inhabited._proof_2}}

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

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

Equations

f.to_fun = λ (x : E), (some_cont_diff_bump_base E).to_fun (f.R / f.r) ((f.r)⁻¹ • (x - c))

@[protected, instance]

noncomputable def cont_diff_bump.has_coe_to_fun {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [has_cont_diff_bump 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]

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

⇑f x = (some_cont_diff_bump_base E).to_fun (f.R / f.r) ((f.r)⁻¹ • (x - c))

@[protected]

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

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

@[protected]

theorem cont_diff_bump.neg {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [has_cont_diff_bump E] (f : cont_diff_bump 0) (x : E) :

⇑f (-x) = ⇑f x

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

⇑f x = 1

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

0 ≤ ⇑f x

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

0 ≤ ⇑f x

A version of cont_diff_bump.nonneg with x explicit

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

⇑f x ≤ 1

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

0 < ⇑f x

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

⇑f x = 0

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

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

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

tsupport ⇑f = metric.closed_ball c f.R

@[protected]

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

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] [has_cont_diff_bump E] {c : E} (f : cont_diff_bump c) {x : E} (h : x ∈ metric.ball c f.r) :

⇑f =ᶠ[nhds x] 1

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

⇑f =ᶠ[nhds c] 1

@[protected]

theorem cont_diff_at.cont_diff_bump {E : Type u_1} {X : Type u_2} [normed_add_comm_group E] [normed_space ℝ E] [normed_add_comm_group X] [normed_space ℝ X] [has_cont_diff_bump E] {n : ℕ∞} {c g : X → E} {f : Π (x : X), cont_diff_bump (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} [normed_add_comm_group E] [normed_space ℝ E] [normed_add_comm_group X] [normed_space ℝ X] [has_cont_diff_bump E] {n : ℕ∞} {c g : X → E} {f : Π (x : X), cont_diff_bump (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.cont_diff {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [has_cont_diff_bump 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] [has_cont_diff_bump E] {c : E} (f : cont_diff_bump c) {x : E} {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] [has_cont_diff_bump E] {c : E} (f : cont_diff_bump c) {x : E} {n : ℕ∞} {s : set E} :

cont_diff_within_at ℝ n ⇑f s x

@[protected]

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

continuous ⇑f

@[protected]

noncomputable def cont_diff_bump.normed {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [has_cont_diff_bump E] {c : E} (f : cont_diff_bump c) [measurable_space E] (μ : measure_theory.measure 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.normed_def {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [has_cont_diff_bump E] {c : E} (f : cont_diff_bump c) [measurable_space E] {μ : measure_theory.measure E} (x : E) :

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

theorem cont_diff_bump.nonneg_normed {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [has_cont_diff_bump E] {c : E} (f : cont_diff_bump c) [measurable_space E] {μ : measure_theory.measure E} (x : E) :

0 ≤ f.normed μ x

theorem cont_diff_bump.cont_diff_normed {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [has_cont_diff_bump E] {c : E} (f : cont_diff_bump c) [measurable_space E] {μ : measure_theory.measure E} {n : ℕ∞} :

cont_diff ℝ n (f.normed μ)

theorem cont_diff_bump.continuous_normed {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [has_cont_diff_bump E] {c : E} (f : cont_diff_bump c) [measurable_space E] {μ : measure_theory.measure E} :

continuous (f.normed μ)

theorem cont_diff_bump.normed_sub {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [has_cont_diff_bump E] {c : E} (f : cont_diff_bump c) [measurable_space E] {μ : measure_theory.measure E} (x : E) :

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

theorem cont_diff_bump.normed_neg {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [has_cont_diff_bump E] [measurable_space E] {μ : measure_theory.measure E} (f : cont_diff_bump 0) (x : E) :

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

@[protected]

theorem cont_diff_bump.integrable {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [has_cont_diff_bump E] {c : E} (f : cont_diff_bump 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.integrable_normed {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [has_cont_diff_bump E] {c : E} (f : cont_diff_bump 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.integral_pos {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [has_cont_diff_bump E] {c : E} (f : cont_diff_bump 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.integral_normed {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [has_cont_diff_bump E] {c : E} (f : cont_diff_bump 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.support_normed_eq {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [has_cont_diff_bump E] {c : E} (f : cont_diff_bump 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.tsupport_normed_eq {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [has_cont_diff_bump E] {c : E} (f : cont_diff_bump 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.has_compact_support_normed {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [has_cont_diff_bump E] {c : E} (f : cont_diff_bump 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.tendsto_support_normed_small_sets {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [has_cont_diff_bump E] {c : E} [measurable_space E] {μ : measure_theory.measure E} [borel_space E] [finite_dimensional ℝ E] [measure_theory.is_locally_finite_measure μ] [μ.is_open_pos_measure] {ι : Type u_2} {φ : ι → cont_diff_bump c} {l : filter ι} (hφ : filter.tendsto (λ (i : ι), (φ i).R) l (nhds 0)) :

filter.tendsto (λ (i : ι), function.support (λ (x : E), (φ i).normed μ x)) l (nhds c).small_sets

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

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