English
Convergence of a localized peak integral toward a local limit at x0 assuming localization to a subset and integrability.
Русский
Сходимость локализованного пикового интеграла к локальному пределу в x0 при локализации и интегрируемости.
LaTeX
$$$\\lim_{i} ∫_{s} φ_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 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_setIntegral_peak_smul_of_integrableOn_of_tendsto (hs : MeasurableSet s) {t : Set α}
(ht : MeasurableSet t) (hts : t ⊆ s) (h'ts : t ∈ 𝓝[s] x₀) (h't : μ t ≠ ∞) (hnφ : ∀ᶠ i in l, ∀ x ∈ s, 0 ≤ φ i 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)) :
Tendsto (fun i : ι ↦ ∫ x in s, φ i x • g x ∂μ) l (𝓝 a) :=
by
let h := g - t.indicator (fun _ ↦ a)
have A : Tendsto (fun i : ι => (∫ x in s, φ i x • h x ∂μ) + (∫ x in t, φ i x ∂μ) • a) l (𝓝 (0 + (1 : ℝ) • a)) :=
by
refine Tendsto.add ?_ (Tendsto.smul hiφ tendsto_const_nhds)
apply tendsto_setIntegral_peak_smul_of_integrableOn_of_tendsto_aux hs ht hts h'ts hnφ hlφ hiφ h'iφ
· apply hmg.sub
simp only [integrable_indicator_iff ht, integrableOn_const_iff (C := a), ht, Measure.restrict_apply]
right
exact lt_of_le_of_lt (measure_mono inter_subset_left) (h't.lt_top)
· rw [← sub_self a]
apply Tendsto.sub hcg
apply tendsto_const_nhds.congr'
filter_upwards [h'ts] with x hx using by simp [hx]
simp only [one_smul, zero_add] at A
refine Tendsto.congr' ?_ A
filter_upwards [integrableOn_peak_smul_of_integrableOn_of_tendsto hs h'ts hlφ hiφ h'iφ hmg hcg,
(tendsto_order.1 (tendsto_iff_norm_sub_tendsto_zero.1 hiφ)).2 1 zero_lt_one] with i hi h'i
simp only [h, Pi.sub_apply, smul_sub, ← indicator_smul_apply]
rw [integral_sub hi, setIntegral_indicator ht, inter_eq_right.mpr hts, integral_smul_const, sub_add_cancel]
rw [integrable_indicator_iff ht]
apply Integrable.smul_const
rw [restrict_restrict ht, inter_eq_left.mpr hts]
exact .of_integral_ne_zero (fun h ↦ by simp [h] at h'i)
