Integrals against peak functions #
A sequence of peak functions is a sequence of functions with average one concentrating around
a point x₀
. Given such a sequence φₙ
, then ∫ φₙ g
tends to g x₀
in many situations, with
a whole zoo of possible assumptions on φₙ
and g
. This file is devoted to such results. Such
functions are also called approximations of unity, or approximations of identity.
Main results #
tendsto_setIntegral_peak_smul_of_integrableOn_of_tendsto
: If a sequence of peak functionsφᵢ
converges uniformly to zero away from a pointx₀
, andg
is integrable and continuous atx₀
, then∫ φᵢ • g
converges tog x₀
.tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_continuousOn
: If a continuous functionc
realizes its maximum at a unique pointx₀
in a compact sets
, then the sequence of functions(c x) ^ n / ∫ (c x) ^ n
is a sequence of peak functions concentrating aroundx₀
. Therefore,∫ (c x) ^ n * g / ∫ (c x) ^ n
converges tog x₀
ifg
is continuous ons
.tendsto_integral_comp_smul_smul_of_integrable
: If a nonnegative functionφ
has integral one and decays quickly enough at infinity, then its renormalizationsx ↦ c ^ d * φ (c • x)
form a sequence of peak functions asc → ∞
. Therefore,∫ (c ^ d * φ (c • x)) • g x
converges tog 0
asc → ∞
ifg
is continuous at0
and integrable.
Note that there are related results about convolution with respect to peak functions in the file
Mathlib.Analysis.Convolution
, such as MeasureTheory.convolution_tendsto_right
there.
General convergent result for integrals against a sequence of peak functions #
If a sequence of peak functions φᵢ
converges uniformly to zero away from a point x₀
, and
g
is integrable and has a limit at x₀
, then φᵢ • g
is eventually integrable.
Alias of integrableOn_peak_smul_of_integrableOn_of_tendsto
.
If a sequence of peak functions φᵢ
converges uniformly to zero away from a point x₀
, and
g
is integrable and has a limit at x₀
, then φᵢ • g
is eventually integrable.
If a sequence of peak functions φᵢ
converges uniformly to zero away from a point x₀
and its
integral on some finite-measure neighborhood of x₀
converges to 1
, and g
is integrable and
has a limit a
at x₀
, then ∫ φᵢ • g
converges to a
.
Auxiliary lemma where one assumes additionally a = 0
.
Alias of tendsto_setIntegral_peak_smul_of_integrableOn_of_tendsto_aux
.
If a sequence of peak functions φᵢ
converges uniformly to zero away from a point x₀
and its
integral on some finite-measure neighborhood of x₀
converges to 1
, and g
is integrable and
has a limit a
at x₀
, then ∫ φᵢ • g
converges to a
.
Auxiliary lemma where one assumes additionally a = 0
.
If a sequence of peak functions φᵢ
converges uniformly to zero away from a point x₀
and its
integral on some finite-measure neighborhood of x₀
converges to 1
, and g
is integrable and
has a limit a
at x₀
, then ∫ φᵢ • g
converges to a
. Version localized to a subset.
Alias of tendsto_setIntegral_peak_smul_of_integrableOn_of_tendsto
.
If a sequence of peak functions φᵢ
converges uniformly to zero away from a point x₀
and its
integral on some finite-measure neighborhood of x₀
converges to 1
, and g
is integrable and
has a limit a
at x₀
, then ∫ φᵢ • g
converges to a
. Version localized to a subset.
If a sequence of peak functions φᵢ
converges uniformly to zero away from a point x₀
and its
integral on some finite-measure neighborhood of x₀
converges to 1
, and g
is integrable and
has a limit a
at x₀
, then ∫ φᵢ • g
converges to a
.
Peak functions of the form x ↦ (c x) ^ n / ∫ (c y) ^ n
#
If a continuous function c
realizes its maximum at a unique point x₀
in a compact set s
,
then the sequence of functions (c x) ^ n / ∫ (c x) ^ n
is a sequence of peak functions
concentrating around x₀
. Therefore, ∫ (c x) ^ n * g / ∫ (c x) ^ n
converges to g x₀
if g
is
integrable on s
and continuous at x₀
.
Version assuming that μ
gives positive mass to all neighborhoods of x₀
within s
.
For a less precise but more usable version, see
tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_continuousOn
.
If a continuous function c
realizes its maximum at a unique point x₀
in a compact set s
,
then the sequence of functions (c x) ^ n / ∫ (c x) ^ n
is a sequence of peak functions
concentrating around x₀
. Therefore, ∫ (c x) ^ n * g / ∫ (c x) ^ n
converges to g x₀
if g
is
integrable on s
and continuous at x₀
.
Version assuming that μ
gives positive mass to all open sets.
For a less precise but more usable version, see
tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_continuousOn
.
If a continuous function c
realizes its maximum at a unique point x₀
in a compact set s
,
then the sequence of functions (c x) ^ n / ∫ (c x) ^ n
is a sequence of peak functions
concentrating around x₀
. Therefore, ∫ (c x) ^ n * g / ∫ (c x) ^ n
converges to g x₀
if g
is
continuous on s
.
Peak functions of the form x ↦ c ^ dim * φ (c x)
#
Consider a nonnegative function φ
with integral one, decaying quickly enough at infinity.
Then suitable renormalizations of φ
form a sequence of peak functions around the origin:
∫ (c ^ d * φ (c • x)) • g x
converges to g 0
as c → ∞
if g
is continuous at 0
and integrable.
Consider a nonnegative function φ
with integral one, decaying quickly enough at infinity.
Then suitable renormalizations of φ
form a sequence of peak functions around any point:
∫ (c ^ d * φ (c • (x₀ - x)) • g x
converges to g x₀
as c → ∞
if g
is continuous at x₀
and integrable.