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 point x₀, and g is integrable and continuous at x₀, then ∫ φᵢ • g converges to g x₀.
• 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.
• tendsto_integral_comp_smul_smul_of_integrable: If a nonnegative function φ has integral one and decays quickly enough at infinity, then its renormalizations x ↦ c ^ d * φ (c • x) form a sequence of peak functions as c → ∞. Therefore, ∫ (c ^ d * φ (c • x)) • g x converges to g 0 as c → ∞ if g is continuous at 0 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

theorem integrableOn_peak_smul_of_integrableOn_of_tendsto {α : Type u_1} {E : Type u_2} {ι : Type u_3} {hm : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace α] [BorelSpace α] [NormedAddCommGroup E] [NormedSpace Real E] {g : α → E} {l : Filter ι} {x₀ : α} {s t : Set α} {φ : ι → α → Real} {a : E} (hs : MeasurableSet s) (h'st : Membership.mem (nhdsWithin x₀ s) t) (hlφ : ∀ (u : Set α), IsOpen u → Membership.mem u x₀ → TendstoUniformlyOn φ 0 l (SDiff.sdiff s u)) (hiφ : Filter.Tendsto (fun (i : ι) => MeasureTheory.integral (μ.restrict t) fun (x : α) => φ i x) l (nhds 1)) (h'iφ : Filter.Eventually (fun (i : ι) => MeasureTheory.AEStronglyMeasurable (φ i) (μ.restrict s)) l) (hmg : MeasureTheory.IntegrableOn g s μ) (hcg : Filter.Tendsto g (nhdsWithin x₀ s) (nhds a)) : Filter.Eventually (fun (i : ι) => MeasureTheory.IntegrableOn (fun (x : α) => HSMul.hSMul (φ i x) (g x)) s μ) l

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.

theorem tendsto_setIntegral_peak_smul_of_integrableOn_of_tendsto_aux {α : Type u_1} {E : Type u_2} {ι : Type u_3} {hm : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace α] [BorelSpace α] [NormedAddCommGroup E] [NormedSpace Real E] {g : α → E} {l : Filter ι} {x₀ : α} {s t : Set α} {φ : ι → α → Real} (hs : MeasurableSet s) (ht : MeasurableSet t) (hts : HasSubset.Subset t s) (h'ts : Membership.mem (nhdsWithin x₀ s) t) (hnφ : Filter.Eventually (fun (i : ι) => ∀ (x : α), Membership.mem s x → LE.le 0 (φ i x)) l) (hlφ : ∀ (u : Set α), IsOpen u → Membership.mem u x₀ → TendstoUniformlyOn φ 0 l (SDiff.sdiff s u)) (hiφ : Filter.Tendsto (fun (i : ι) => MeasureTheory.integral (μ.restrict t) fun (x : α) => φ i x) l (nhds 1)) (h'iφ : Filter.Eventually (fun (i : ι) => MeasureTheory.AEStronglyMeasurable (φ i) (μ.restrict s)) l) (hmg : MeasureTheory.IntegrableOn g s μ) (hcg : Filter.Tendsto g (nhdsWithin x₀ s) (nhds 0)) : Filter.Tendsto (fun (i : ι) => MeasureTheory.integral (μ.restrict s) fun (x : α) => HSMul.hSMul (φ i x) (g x)) l (nhds 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. Auxiliary lemma where one assumes additionally a = 0.

theorem tendsto_setIntegral_peak_smul_of_integrableOn_of_tendsto {α : Type u_1} {E : Type u_2} {ι : Type u_3} {hm : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace α] [BorelSpace α] [NormedAddCommGroup E] [NormedSpace Real E] {g : α → E} {l : Filter ι} {x₀ : α} {s : Set α} {φ : ι → α → Real} {a : E} [CompleteSpace E] (hs : MeasurableSet s) {t : Set α} (ht : MeasurableSet t) (hts : HasSubset.Subset t s) (h'ts : Membership.mem (nhdsWithin x₀ s) t) (h't : Ne (DFunLike.coe μ t) Top.top) (hnφ : Filter.Eventually (fun (i : ι) => ∀ (x : α), Membership.mem s x → LE.le 0 (φ i x)) l) (hlφ : ∀ (u : Set α), IsOpen u → Membership.mem u x₀ → TendstoUniformlyOn φ 0 l (SDiff.sdiff s u)) (hiφ : Filter.Tendsto (fun (i : ι) => MeasureTheory.integral (μ.restrict t) fun (x : α) => φ i x) l (nhds 1)) (h'iφ : Filter.Eventually (fun (i : ι) => MeasureTheory.AEStronglyMeasurable (φ i) (μ.restrict s)) l) (hmg : MeasureTheory.IntegrableOn g s μ) (hcg : Filter.Tendsto g (nhdsWithin x₀ s) (nhds a)) : Filter.Tendsto (fun (i : ι) => MeasureTheory.integral (μ.restrict s) fun (x : α) => HSMul.hSMul (φ i x) (g x)) l (nhds a)

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.

theorem tendsto_integral_peak_smul_of_integrable_of_tendsto {α : Type u_1} {E : Type u_2} {ι : Type u_3} {hm : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace α] [BorelSpace α] [NormedAddCommGroup E] [NormedSpace Real E] {g : α → E} {l : Filter ι} {x₀ : α} {φ : ι → α → Real} {a : E} [CompleteSpace E] {t : Set α} (ht : MeasurableSet t) (h'ts : Membership.mem (nhds x₀) t) (h't : Ne (DFunLike.coe μ t) Top.top) (hnφ : Filter.Eventually (fun (i : ι) => ∀ (x : α), LE.le 0 (φ i x)) l) (hlφ : ∀ (u : Set α), IsOpen u → Membership.mem u x₀ → TendstoUniformlyOn φ 0 l (HasCompl.compl u)) (hiφ : Filter.Tendsto (fun (i : ι) => MeasureTheory.integral (μ.restrict t) fun (x : α) => φ i x) l (nhds 1)) (h'iφ : Filter.Eventually (fun (i : ι) => MeasureTheory.AEStronglyMeasurable (φ i) μ) l) (hmg : MeasureTheory.Integrable g μ) (hcg : Filter.Tendsto g (nhds x₀) (nhds a)) : Filter.Tendsto (fun (i : ι) => MeasureTheory.integral μ fun (x : α) => HSMul.hSMul (φ i x) (g x)) l (nhds a)

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

theorem tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_measure_nhdsWithin_pos {α : Type u_1} {E : Type u_2} {hm : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace α] [BorelSpace α] [NormedAddCommGroup E] [NormedSpace Real E] {g : α → E} {x₀ : α} {s : Set α} [CompleteSpace E] [TopologicalSpace.MetrizableSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] (hs : IsCompact s) (hμ : ∀ (u : Set α), IsOpen u → Membership.mem u x₀ → LT.lt 0 (DFunLike.coe μ (Inter.inter u s))) {c : α → Real} (hc : ContinuousOn c s) (h'c : ∀ (y : α), Membership.mem s y → Ne y x₀ → LT.lt (c y) (c x₀)) (hnc : ∀ (x : α), Membership.mem s x → LE.le 0 (c x)) (hnc₀ : LT.lt 0 (c x₀)) (h₀ : Membership.mem s x₀) (hmg : MeasureTheory.IntegrableOn g s μ) (hcg : ContinuousWithinAt g s x₀) : Filter.Tendsto (fun (n : Nat) => HSMul.hSMul (Inv.inv (MeasureTheory.integral (μ.restrict s) fun (x : α) => HPow.hPow (c x) n)) (MeasureTheory.integral (μ.restrict s) fun (x : α) => HSMul.hSMul (HPow.hPow (c x) n) (g x))) Filter.atTop (nhds (g x₀))

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.

theorem tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_integrableOn {α : Type u_1} {E : Type u_2} {hm : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace α] [BorelSpace α] [NormedAddCommGroup E] [NormedSpace Real E] {g : α → E} {x₀ : α} {s : Set α} [CompleteSpace E] [TopologicalSpace.MetrizableSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] [μ.IsOpenPosMeasure] (hs : IsCompact s) {c : α → Real} (hc : ContinuousOn c s) (h'c : ∀ (y : α), Membership.mem s y → Ne y x₀ → LT.lt (c y) (c x₀)) (hnc : ∀ (x : α), Membership.mem s x → LE.le 0 (c x)) (hnc₀ : LT.lt 0 (c x₀)) (h₀ : Membership.mem (closure (interior s)) x₀) (hmg : MeasureTheory.IntegrableOn g s μ) (hcg : ContinuousWithinAt g s x₀) : Filter.Tendsto (fun (n : Nat) => HSMul.hSMul (Inv.inv (MeasureTheory.integral (μ.restrict s) fun (x : α) => HPow.hPow (c x) n)) (MeasureTheory.integral (μ.restrict s) fun (x : α) => HSMul.hSMul (HPow.hPow (c x) n) (g x))) Filter.atTop (nhds (g x₀))

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.

theorem tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_continuousOn {α : Type u_1} {E : Type u_2} {hm : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace α] [BorelSpace α] [NormedAddCommGroup E] [NormedSpace Real E] {g : α → E} {x₀ : α} {s : Set α} [CompleteSpace E] [TopologicalSpace.MetrizableSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] [μ.IsOpenPosMeasure] (hs : IsCompact s) {c : α → Real} (hc : ContinuousOn c s) (h'c : ∀ (y : α), Membership.mem s y → Ne y x₀ → LT.lt (c y) (c x₀)) (hnc : ∀ (x : α), Membership.mem s x → LE.le 0 (c x)) (hnc₀ : LT.lt 0 (c x₀)) (h₀ : Membership.mem (closure (interior s)) x₀) (hmg : ContinuousOn g s) : Filter.Tendsto (fun (n : Nat) => HSMul.hSMul (Inv.inv (MeasureTheory.integral (μ.restrict s) fun (x : α) => HPow.hPow (c x) n)) (MeasureTheory.integral (μ.restrict s) fun (x : α) => HSMul.hSMul (HPow.hPow (c x) n) (g x))) Filter.atTop (nhds (g x₀))

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)

theorem tendsto_integral_comp_smul_smul_of_integrable {E : Type u_2} [NormedAddCommGroup E] [NormedSpace Real E] [CompleteSpace E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace Real F] [FiniteDimensional Real F] [MeasurableSpace F] [BorelSpace F] {μ : MeasureTheory.Measure F} [μ.IsAddHaarMeasure] {φ : F → Real} (hφ : ∀ (x : F), LE.le 0 (φ x)) (h'φ : Eq (MeasureTheory.integral μ fun (x : F) => φ x) 1) (h : Filter.Tendsto (fun (x : F) => HMul.hMul (HPow.hPow (Norm.norm x) (Module.finrank Real F)) (φ x)) (Bornology.cobounded F) (nhds 0)) {g : F → E} (hg : MeasureTheory.Integrable g μ) (h'g : ContinuousAt g 0) : Filter.Tendsto (fun (c : Real) => MeasureTheory.integral μ fun (x : F) => HSMul.hSMul (HMul.hMul (HPow.hPow c (Module.finrank Real F)) (φ (HSMul.hSMul c x))) (g x)) Filter.atTop (nhds (g 0))

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.

theorem tendsto_integral_comp_smul_smul_of_integrable' {E : Type u_2} [NormedAddCommGroup E] [NormedSpace Real E] [CompleteSpace E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace Real F] [FiniteDimensional Real F] [MeasurableSpace F] [BorelSpace F] {μ : MeasureTheory.Measure F} [μ.IsAddHaarMeasure] {φ : F → Real} (hφ : ∀ (x : F), LE.le 0 (φ x)) (h'φ : Eq (MeasureTheory.integral μ fun (x : F) => φ x) 1) (h : Filter.Tendsto (fun (x : F) => HMul.hMul (HPow.hPow (Norm.norm x) (Module.finrank Real F)) (φ x)) (Bornology.cobounded F) (nhds 0)) {g : F → E} {x₀ : F} (hg : MeasureTheory.Integrable g μ) (h'g : ContinuousAt g x₀) : Filter.Tendsto (fun (c : Real) => MeasureTheory.integral μ fun (x : F) => HSMul.hSMul (HMul.hMul (HPow.hPow c (Module.finrank Real F)) (φ (HSMul.hSMul c (HSub.hSub x₀ x)))) (g x)) Filter.atTop (nhds (g x₀))

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.