Integrals against peak functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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_integrable_on_of_continuous_within_at: 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_is_compact_of_continuous_on: 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.

source

theorem set.disjoint_sdiff_inter {α : Type u_1} (s 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.

source

theorem integrable_on_peak_smul_of_integrable_on_of_continuous_within_at {α : Type u_1} {E : Type u_2} {ι : Type u_3} {hm : measurable_space α} {μ : measure_theory.measure α} [topological_space α] [borel_space α] [normed_add_comm_group E] [normed_space ℝ E] {g : α → E} {l : filter ι} {x₀ : α} {s : set α} {φ : ι → α → ℝ} (hs : measurable_set s) (hlφ : ∀ (u : set α), is_open u → x₀ ∈ u → tendsto_uniformly_on φ 0 l (s \ u)) (hiφ : ∀ᶠ (i : ι) in l, ∫ (x : α) in s, φ i x ∂μ = 1) (hmg : measure_theory.integrable_on g s μ) (hcg : continuous_within_at g s x₀) :

∀ᶠ (i : ι) in l, measure_theory.integrable_on (λ (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.

source

theorem tendsto_set_integral_peak_smul_of_integrable_on_of_continuous_within_at_aux {α : Type u_1} {E : Type u_2} {ι : Type u_3} {hm : measurable_space α} {μ : measure_theory.measure α} [topological_space α] [borel_space α] [normed_add_comm_group E] [normed_space ℝ E] {g : α → E} {l : filter ι} {x₀ : α} {s : set α} {φ : ι → α → ℝ} [complete_space E] (hs : measurable_set s) (hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x) (hlφ : ∀ (u : set α), is_open u → x₀ ∈ u → tendsto_uniformly_on φ 0 l (s \ u)) (hiφ : ∀ᶠ (i : ι) in l, ∫ (x : α) in s, φ i x ∂μ = 1) (hmg : measure_theory.integrable_on g s μ) (h'g : g x₀ = 0) (hcg : continuous_within_at g s x₀) :

filter.tendsto (λ (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.

source

theorem tendsto_set_integral_peak_smul_of_integrable_on_of_continuous_within_at {α : Type u_1} {E : Type u_2} {ι : Type u_3} {hm : measurable_space α} {μ : measure_theory.measure α} [topological_space α] [borel_space α] [normed_add_comm_group E] [normed_space ℝ E] {g : α → E} {l : filter ι} {x₀ : α} {s : set α} {φ : ι → α → ℝ} [complete_space E] (hs : measurable_set s) (h's : ⇑μ s ≠ ⊤) (hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x) (hlφ : ∀ (u : set α), is_open u → x₀ ∈ u → tendsto_uniformly_on φ 0 l (s \ u)) (hiφ : (λ (i : ι), ∫ (x : α) in s, φ i x ∂μ) =ᶠ[l] 1) (hmg : measure_theory.integrable_on g s μ) (hcg : continuous_within_at g s x₀) :

filter.tendsto (λ (i : ι), ∫ (x : α) in s, φ i x • g x ∂μ) l (nhds (g x₀))

source

theorem tendsto_set_integral_pow_smul_of_unique_maximum_of_is_compact_of_measure_nhds_within_pos {α : Type u_1} {E : Type u_2} {hm : measurable_space α} {μ : measure_theory.measure α} [topological_space α] [borel_space α] [normed_add_comm_group E] [normed_space ℝ E] {g : α → E} {x₀ : α} {s : set α} [complete_space E] [topological_space.metrizable_space α] [measure_theory.is_locally_finite_measure μ] (hs : is_compact s) (hμ : ∀ (u : set α), is_open u → x₀ ∈ u → 0 < ⇑μ (u ∩ s)) {c : α → ℝ} (hc : continuous_on c s) (h'c : ∀ (y : α), y ∈ s → y ≠ x₀ → c y < c x₀) (hnc : ∀ (x : α), x ∈ s → 0 ≤ c x) (hnc₀ : 0 < c x₀) (h₀ : x₀ ∈ s) (hmg : measure_theory.integrable_on g s μ) (hcg : continuous_within_at g s x₀) :

filter.tendsto (λ (n : ℕ), (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ • ∫ (x : α) in s, c x ^ n • g x ∂μ) filter.at_top (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_is_compact_of_continuous_on.

source

theorem tendsto_set_integral_pow_smul_of_unique_maximum_of_is_compact_of_integrable_on {α : Type u_1} {E : Type u_2} {hm : measurable_space α} {μ : measure_theory.measure α} [topological_space α] [borel_space α] [normed_add_comm_group E] [normed_space ℝ E] {g : α → E} {x₀ : α} {s : set α} [complete_space E] [topological_space.metrizable_space α] [measure_theory.is_locally_finite_measure μ] [μ.is_open_pos_measure] (hs : is_compact s) {c : α → ℝ} (hc : continuous_on c s) (h'c : ∀ (y : α), y ∈ s → y ≠ x₀ → c y < c x₀) (hnc : ∀ (x : α), x ∈ s → 0 ≤ c x) (hnc₀ : 0 < c x₀) (h₀ : x₀ ∈ closure (interior s)) (hmg : measure_theory.integrable_on g s μ) (hcg : continuous_within_at g s x₀) :

filter.tendsto (λ (n : ℕ), (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ • ∫ (x : α) in s, c x ^ n • g x ∂μ) filter.at_top (nhds (g 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_is_compact_of_continuous_on.

source

theorem tendsto_set_integral_pow_smul_of_unique_maximum_of_is_compact_of_continuous_on {α : Type u_1} {E : Type u_2} {hm : measurable_space α} {μ : measure_theory.measure α} [topological_space α] [borel_space α] [normed_add_comm_group E] [normed_space ℝ E] {g : α → E} {x₀ : α} {s : set α} [complete_space E] [topological_space.metrizable_space α] [measure_theory.is_locally_finite_measure μ] [μ.is_open_pos_measure] (hs : is_compact s) {c : α → ℝ} (hc : continuous_on c s) (h'c : ∀ (y : α), y ∈ s → y ≠ x₀ → c y < c x₀) (hnc : ∀ (x : α), x ∈ s → 0 ≤ c x) (hnc₀ : 0 < c x₀) (h₀ : x₀ ∈ closure (interior s)) (hmg : continuous_on g s) :

filter.tendsto (λ (n : ℕ), (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ • ∫ (x : α) in s, c x ^ n • g x ∂μ) filter.at_top (nhds (g x₀))