mathlib documentation

geometry.manifold.bump_function

Smooth bump functions on a smooth manifold #

In this file we define smooth_bump_function I c to be a bundled smooth "bump" function centered at c. It is a structure that consists of two real numbers 0 < r < R with small enough R. We define a coercion to function for this type, and for f : smooth_bump_function I c, the function ⇑f written in the extended chart at c has the following properties:

The actual statements involve (pre)images under ext_chart_at I f and are given as lemmas in the smooth_bump_function namespace.

Tags #

manifold, smooth bump function

Smooth bump function #

In this section we define a structure for a bundled smooth bump function and prove its properties.

structure smooth_bump_function {E : Type uE} [normed_add_comm_group E] [normed_space E] [finite_dimensional E] {H : Type uH} [topological_space H] (I : model_with_corners E H) {M : Type uM} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] (c : M) :
Type

Given a smooth manifold modelled on a finite dimensional space E, f : smooth_bump_function I M is a smooth function on M such that in the extended chart e at f.c:

  • f x = 1 in the closed euclidean ball of radius f.r centered at f.c;
  • f x = 0 outside of the euclidean ball of radius f.R centered at f.c;
  • 0 ≤ f x ≤ 1 for all x.

The structure contains data required to construct a function with these properties. The function is available as ⇑f or f x. Formal statements of the properties listed above involve some (pre)images under ext_chart_at I f.c and are given as lemmas in the smooth_bump_function namespace.

Instances for smooth_bump_function
noncomputable def smooth_bump_function.to_fun {E : Type uE} [normed_add_comm_group E] [normed_space E] [finite_dimensional E] {H : Type uH} [topological_space H] {I : model_with_corners E H} {M : Type uM} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {c : M} (f : smooth_bump_function I c) :
M →

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

Equations
theorem smooth_bump_function.nonneg {E : Type uE} [normed_add_comm_group E] [normed_space E] [finite_dimensional E] {H : Type uH} [topological_space H] {I : model_with_corners E H} {M : Type uM} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {c : M} (f : smooth_bump_function I c) {x : M} :
0 f x
theorem smooth_bump_function.le_one {E : Type uE} [normed_add_comm_group E] [normed_space E] [finite_dimensional E] {H : Type uH} [topological_space H] {I : model_with_corners E H} {M : Type uM} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {c : M} (f : smooth_bump_function I c) {x : M} :
f x 1
@[simp]

Given a smooth bump function f : smooth_bump_function I c, the closed ball of radius f.R is known to include the support of f. These closed balls (in the model normed space E) intersected with set.range I form a basis of 𝓝[range I] (ext_chart_at I c c).

If f is a smooth bump function and s closed subset of the support of f (i.e., of the open ball of radius f.R), then there exists 0 < r < f.R such that s is a subset of the open ball of radius r. Formally, s ⊆ e.source ∩ e ⁻¹' (ball (e c) r), where e = ext_chart_at I c.

Replace r with another value in the interval (0, f.R).

Equations
@[protected, instance]
Equations

The closures of supports of smooth bump functions centered at c form a basis of 𝓝 c. In other words, each of these closures is a neighborhood of c and each neighborhood of c includes tsupport f for some f : smooth_bump_function I c.

Given s ∈ 𝓝 c, the supports of smooth bump functions f : smooth_bump_function I c such that tsupport f ⊆ s form a basis of 𝓝 c. In other words, each of these supports is a neighborhood of c and each neighborhood of c includes support f for some f : smooth_bump_function I c such that tsupport f ⊆ s.

@[protected]

A smooth bump function is infinitely smooth.

If f : smooth_bump_function I c is a smooth bump function and g : M → G is a function smooth on the source of the chart at c, then f • g is smooth on the whole manifold.