# 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 Analysis.Convolution, such as 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 : } {μ : } [] [] [] {g : αE} {l : } {x₀ : α} {s : Set α} {t : Set α} {φ : ια} {a : E} (hs : ) (h'st : t nhdsWithin x₀ s) (hlφ : ∀ (u : Set α), x₀ uTendstoUniformlyOn φ 0 l (s \ u)) (hiφ : Filter.Tendsto (fun (i : ι) => ∫ (x : α) in t, φ i xμ) l (nhds 1)) (h'iφ : ∀ᶠ (i : ι) in l, MeasureTheory.AEStronglyMeasurable (φ i) (μ.restrict s)) (hmg : ) (hcg : Filter.Tendsto g (nhdsWithin x₀ s) (nhds a)) :
∀ᶠ (i : ι) in l, MeasureTheory.IntegrableOn (fun (x : α) => φ i x g x) s μ

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.

@[deprecated integrableOn_peak_smul_of_integrableOn_of_tendsto]
theorem integrableOn_peak_smul_of_integrableOn_of_continuousWithinAt {α : Type u_1} {E : Type u_2} {ι : Type u_3} {hm : } {μ : } [] [] [] {g : αE} {l : } {x₀ : α} {s : Set α} {t : Set α} {φ : ια} {a : E} (hs : ) (h'st : t nhdsWithin x₀ s) (hlφ : ∀ (u : Set α), x₀ uTendstoUniformlyOn φ 0 l (s \ u)) (hiφ : Filter.Tendsto (fun (i : ι) => ∫ (x : α) in t, φ i xμ) l (nhds 1)) (h'iφ : ∀ᶠ (i : ι) in l, MeasureTheory.AEStronglyMeasurable (φ i) (μ.restrict s)) (hmg : ) (hcg : Filter.Tendsto g (nhdsWithin x₀ s) (nhds a)) :
∀ᶠ (i : ι) in l, MeasureTheory.IntegrableOn (fun (x : α) => φ i x g x) s μ

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.

theorem tendsto_setIntegral_peak_smul_of_integrableOn_of_tendsto_aux {α : Type u_1} {E : Type u_2} {ι : Type u_3} {hm : } {μ : } [] [] [] {g : αE} {l : } {x₀ : α} {s : Set α} {t : Set α} {φ : ια} (hs : ) (ht : ) (hts : t s) (h'ts : t nhdsWithin x₀ s) (hnφ : ∀ᶠ (i : ι) in l, xs, 0 φ i x) (hlφ : ∀ (u : Set α), x₀ uTendstoUniformlyOn φ 0 l (s \ u)) (hiφ : Filter.Tendsto (fun (i : ι) => ∫ (x : α) in t, φ i xμ) l (nhds 1)) (h'iφ : ∀ᶠ (i : ι) in l, MeasureTheory.AEStronglyMeasurable (φ i) (μ.restrict s)) (hmg : ) (hcg : Filter.Tendsto g (nhdsWithin x₀ s) (nhds 0)) :
Filter.Tendsto (fun (i : ι) => ∫ (x : α) in s, φ 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.

@[deprecated tendsto_setIntegral_peak_smul_of_integrableOn_of_tendsto_aux]
theorem tendsto_setIntegral_peak_smul_of_integrableOn_of_continuousWithinAt_aux {α : Type u_1} {E : Type u_2} {ι : Type u_3} {hm : } {μ : } [] [] [] {g : αE} {l : } {x₀ : α} {s : Set α} {t : Set α} {φ : ια} (hs : ) (ht : ) (hts : t s) (h'ts : t nhdsWithin x₀ s) (hnφ : ∀ᶠ (i : ι) in l, xs, 0 φ i x) (hlφ : ∀ (u : Set α), x₀ uTendstoUniformlyOn φ 0 l (s \ u)) (hiφ : Filter.Tendsto (fun (i : ι) => ∫ (x : α) in t, φ i xμ) l (nhds 1)) (h'iφ : ∀ᶠ (i : ι) in l, MeasureTheory.AEStronglyMeasurable (φ i) (μ.restrict s)) (hmg : ) (hcg : Filter.Tendsto g (nhdsWithin x₀ s) (nhds 0)) :
Filter.Tendsto (fun (i : ι) => ∫ (x : α) in s, φ i x g xμ) l (nhds 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.

theorem tendsto_setIntegral_peak_smul_of_integrableOn_of_tendsto {α : Type u_1} {E : Type u_2} {ι : Type u_3} {hm : } {μ : } [] [] [] {g : αE} {l : } {x₀ : α} {s : Set α} {φ : ια} {a : E} [] (hs : ) {t : Set α} (ht : ) (hts : t s) (h'ts : t nhdsWithin x₀ s) (h't : μ t ) (hnφ : ∀ᶠ (i : ι) in l, xs, 0 φ i x) (hlφ : ∀ (u : Set α), x₀ uTendstoUniformlyOn φ 0 l (s \ u)) (hiφ : Filter.Tendsto (fun (i : ι) => ∫ (x : α) in t, φ i xμ) l (nhds 1)) (h'iφ : ∀ᶠ (i : ι) in l, MeasureTheory.AEStronglyMeasurable (φ i) (μ.restrict s)) (hmg : ) (hcg : Filter.Tendsto g (nhdsWithin x₀ s) (nhds a)) :
Filter.Tendsto (fun (i : ι) => ∫ (x : α) in s, φ 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.

@[deprecated tendsto_setIntegral_peak_smul_of_integrableOn_of_tendsto]
theorem tendsto_setIntegral_peak_smul_of_integrableOn_of_continuousWithinAt {α : Type u_1} {E : Type u_2} {ι : Type u_3} {hm : } {μ : } [] [] [] {g : αE} {l : } {x₀ : α} {s : Set α} {φ : ια} {a : E} [] (hs : ) {t : Set α} (ht : ) (hts : t s) (h'ts : t nhdsWithin x₀ s) (h't : μ t ) (hnφ : ∀ᶠ (i : ι) in l, xs, 0 φ i x) (hlφ : ∀ (u : Set α), x₀ uTendstoUniformlyOn φ 0 l (s \ u)) (hiφ : Filter.Tendsto (fun (i : ι) => ∫ (x : α) in t, φ i xμ) l (nhds 1)) (h'iφ : ∀ᶠ (i : ι) in l, MeasureTheory.AEStronglyMeasurable (φ i) (μ.restrict s)) (hmg : ) (hcg : Filter.Tendsto g (nhdsWithin x₀ s) (nhds a)) :
Filter.Tendsto (fun (i : ι) => ∫ (x : α) in s, φ i x g xμ) l (nhds a)

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.

theorem tendsto_integral_peak_smul_of_integrable_of_tendsto {α : Type u_1} {E : Type u_2} {ι : Type u_3} {hm : } {μ : } [] [] [] {g : αE} {l : } {x₀ : α} {φ : ια} {a : E} [] {t : Set α} (ht : ) (h'ts : t nhds x₀) (h't : μ t ) (hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), 0 φ i x) (hlφ : ∀ (u : Set α), x₀ u) (hiφ : Filter.Tendsto (fun (i : ι) => ∫ (x : α) in t, φ i xμ) l (nhds 1)) (h'iφ : ∀ᶠ (i : ι) in l, ) (hmg : ) (hcg : Filter.Tendsto g (nhds x₀) (nhds a)) :
Filter.Tendsto (fun (i : ι) => ∫ (x : α), φ 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 : } {μ : } [] [] [] {g : αE} {x₀ : α} {s : Set α} [] (hs : ) (hμ : ∀ (u : Set α), x₀ u0 < μ (u s)) {c : α} (hc : ) (h'c : ys, y x₀c y < c x₀) (hnc : xs, 0 c x) (hnc₀ : 0 < c x₀) (h₀ : x₀ s) (hmg : ) (hcg : ) :
Filter.Tendsto (fun (n : ) => (∫ (x : α) in s, c x ^ nμ)⁻¹ ∫ (x : α) in s, 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 : } {μ : } [] [] [] {g : αE} {x₀ : α} {s : Set α} [] [μ.IsOpenPosMeasure] (hs : ) {c : α} (hc : ) (h'c : ys, y x₀c y < c x₀) (hnc : xs, 0 c x) (hnc₀ : 0 < c x₀) (h₀ : x₀ closure ()) (hmg : ) (hcg : ) :
Filter.Tendsto (fun (n : ) => (∫ (x : α) in s, c x ^ nμ)⁻¹ ∫ (x : α) in s, 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 : } {μ : } [] [] [] {g : αE} {x₀ : α} {s : Set α} [] [μ.IsOpenPosMeasure] (hs : ) {c : α} (hc : ) (h'c : ys, y x₀c y < c x₀) (hnc : xs, 0 c x) (hnc₀ : 0 < c x₀) (h₀ : x₀ closure ()) (hmg : ) :
Filter.Tendsto (fun (n : ) => (∫ (x : α) in s, c x ^ nμ)⁻¹ ∫ (x : α) in s, 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} [] [] {F : Type u_4} [] [] [] [] {μ : } [μ.IsAddHaarMeasure] {φ : F} (hφ : ∀ (x : F), 0 φ x) (h'φ : ∫ (x : F), φ xμ = 1) (h : Filter.Tendsto (fun (x : F) => * φ x) (nhds 0)) {g : FE} (hg : ) (h'g : ) :
Filter.Tendsto (fun (c : ) => ∫ (x : F), ( * φ (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} [] [] {F : Type u_4} [] [] [] [] {μ : } [μ.IsAddHaarMeasure] {φ : F} (hφ : ∀ (x : F), 0 φ x) (h'φ : ∫ (x : F), φ xμ = 1) (h : Filter.Tendsto (fun (x : F) => * φ x) (nhds 0)) {g : FE} {x₀ : F} (hg : ) (h'g : ContinuousAt g x₀) :
Filter.Tendsto (fun (c : ) => ∫ (x : F), ( * φ (c (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.