English
A concentrated peak lemma showing that concentrating near a point yields convergence of integrals with smoothed weights.
Русский
Лемма пика интеграла: сосредоточение около точки приводит к сходимости интегралов со сглаженными весами.
LaTeX
$$$\\lim_{i} ∫ φ_i(x) g(x) dx = g(x_0)$ при условии нормализации и сходимости весов.$$
Lean4
/-- 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 integrableOn_peak_smul_of_integrableOn_of_tendsto (hs : MeasurableSet s) (h'st : t ∈ 𝓝[s] x₀)
(hlφ : ∀ u : Set α, IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u))
(hiφ : Tendsto (fun i ↦ ∫ x in t, φ i x ∂μ) l (𝓝 1)) (h'iφ : ∀ᶠ i in l, AEStronglyMeasurable (φ i) (μ.restrict s))
(hmg : IntegrableOn g s μ) (hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)) : ∀ᶠ i in l, IntegrableOn (fun x => φ i x • g x) s μ :=
by
obtain ⟨u, u_open, x₀u, ut, hu⟩ : ∃ u, IsOpen u ∧ x₀ ∈ u ∧ s ∩ u ⊆ t ∧ ∀ x ∈ u ∩ s, g x ∈ ball a 1 :=
by
rcases mem_nhdsWithin.1 (Filter.inter_mem h'st (hcg (ball_mem_nhds _ zero_lt_one))) with ⟨u, u_open, x₀u, hu⟩
refine ⟨u, u_open, x₀u, ?_, hu.trans inter_subset_right⟩
rw [inter_comm]
exact hu.trans inter_subset_left
rw [tendsto_iff_norm_sub_tendsto_zero] at hiφ
filter_upwards [tendstoUniformlyOn_iff.1 (hlφ u u_open x₀u) 1 zero_lt_one, (tendsto_order.1 hiφ).2 1 zero_lt_one,
h'iφ] with i hi h'i h''i
have I : IntegrableOn (φ i) t μ := .of_integral_ne_zero (fun h ↦ by simp [h] at h'i)
have A : IntegrableOn (fun x => φ i x • g x) (s \ u) μ :=
by
refine Integrable.smul_of_top_right (hmg.mono diff_subset le_rfl) ?_
apply memLp_top_of_bound (h''i.mono_set diff_subset) 1
filter_upwards [self_mem_ae_restrict (hs.diff u_open.measurableSet)] with x hx
simpa only [Pi.zero_apply, dist_zero_left] using (hi x hx).le
have B : IntegrableOn (fun x => φ i x • g x) (s ∩ u) μ :=
by
apply Integrable.smul_of_top_left
· exact IntegrableOn.mono_set I ut
· apply memLp_top_of_bound (hmg.mono_set inter_subset_left).aestronglyMeasurable (‖a‖ + 1)
filter_upwards [self_mem_ae_restrict (hs.inter u_open.measurableSet)] with x hx
rw [inter_comm] at hx
exact (norm_lt_of_mem_ball (hu x hx)).le
convert A.union B
simp only [diff_union_inter]
