# Documentation

Mathlib.MeasureTheory.Integral.PeakFunction

# 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.

## Main results #

• tendsto_set_integral_peak_smul_of_integrableOn_of_continuousWithinAt: 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_set_integral_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.

Note that there are related results about convolution with respect to peak functions in the file Analysis.Convolution, such as convolution_tendsto_right there.

theorem Set.disjoint_sdiff_inter {α : Type u_1} (s : Set α) (t : Set α) :
Disjoint (s \ t) (s t)

This lemma exists for finsets, but not for sets currently. porting note: move to data.set.basic after the port.

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 α} {φ : ια} (hs : ) (hlφ : ∀ (u : Set α), x₀ uTendstoUniformlyOn φ 0 l (s \ u)) (hiφ : ∀ᶠ (i : ι) in l, ∫ (x : α) in s, φ i xμ = 1) (hmg : ) (hcg : ) :
∀ᶠ (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 continuous at x₀, then φᵢ • g is eventually integrable.

theorem tendsto_set_integral_peak_smul_of_integrableOn_of_continuousWithinAt_aux {α : Type u_1} {E : Type u_2} {ι : Type u_3} {hm : } {μ : } [] [] [] {g : αE} {l : } {x₀ : α} {s : Set α} {φ : ια} (hs : ) (hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x s0 φ i x) (hlφ : ∀ (u : Set α), x₀ uTendstoUniformlyOn φ 0 l (s \ u)) (hiφ : ∀ᶠ (i : ι) in l, ∫ (x : α) in s, φ i xμ = 1) (hmg : ) (h'g : g x₀ = 0) (hcg : ) :
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 g is integrable and continuous at x₀, then ∫ φᵢ • g converges to x₀. Auxiliary lemma where one assumes additionally g x₀ = 0.

theorem tendsto_set_integral_peak_smul_of_integrableOn_of_continuousWithinAt {α : Type u_1} {E : Type u_2} {ι : Type u_3} {hm : } {μ : } [] [] [] {g : αE} {l : } {x₀ : α} {s : Set α} {φ : ια} [] (hs : ) (h's : μ s ) (hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x s0 φ i x) (hlφ : ∀ (u : Set α), x₀ uTendstoUniformlyOn φ 0 l (s \ u)) (hiφ : (fun i => ∫ (x : α) in s, φ i xμ) =ᶠ[l] 1) (hmg : ) (hcg : ) :
Filter.Tendsto (fun i => ∫ (x : α) in s, φ i x g xμ) l (nhds (g x₀))
theorem tendsto_set_integral_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 : ∀ (y : α), y sy x₀c y < c x₀) (hnc : ∀ (x : α), x s0 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_set_integral_pow_smul_of_unique_maximum_of_isCompact_of_continuousOn.

theorem tendsto_set_integral_pow_smul_of_unique_maximum_of_isCompact_of_integrableOn {α : Type u_1} {E : Type u_2} {hm : } {μ : } [] [] [] {g : αE} {x₀ : α} {s : Set α} [] (hs : ) {c : α} (hc : ) (h'c : ∀ (y : α), y sy x₀c y < c x₀) (hnc : ∀ (x : α), x s0 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_set_integral_pow_smul_of_unique_maximum_of_isCompact_of_continuousOn.

theorem tendsto_set_integral_pow_smul_of_unique_maximum_of_isCompact_of_continuousOn {α : Type u_1} {E : Type u_2} {hm : } {μ : } [] [] [] {g : αE} {x₀ : α} {s : Set α} [] (hs : ) {c : α} (hc : ) (h'c : ∀ (y : α), y sy x₀c y < c x₀) (hnc : ∀ (x : α), x s0 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.