English
Let κ be a kernel and ν a dominating kernel with fst κ ≤ ν. For a fixed a ∈ α and an antitone sequence seq: ℕ → Set β of measurable sets whose intersection is empty, the integral of the density κ ν over seq m against ν a tends to 0 as m → ∞.
Русский
Пусть κ и ν — ядра, причём fst κ ≤ ν. Пусть для некоторого a ∈ α имеется антимонотонная последовательность seq: ℕ → множество β с измеримыми первопричинами, удовлетворяющая ⋂ seq i = ∅. Тогда интеграл плотности κ ν по seq m относительно ν a стремится к 0 при m → ∞.
LaTeX
$$$\\operatorname{Tendsto}\\Bigl(m \\mapsto \\int x\\, \\density_{\\kappa,\\nu}(a,x)(\\mathrm{seq}(m))\\, \\partial(\\nu a)\\Bigr)\\_{\\operatorname{atTop}} \\;=\\; 0$$$
Lean4
theorem tendsto_integral_density_of_antitone (hκν : fst κ ≤ ν) [IsFiniteKernel ν] (a : α) (seq : ℕ → Set β)
(hseq : Antitone seq) (hseq_iInter : ⋂ i, seq i = ∅) (hseq_meas : ∀ m, MeasurableSet (seq m)) :
Tendsto (fun m ↦ ∫ x, density κ ν a x (seq m) ∂(ν a)) atTop (𝓝 0) :=
by
have : IsFiniteKernel κ := isFiniteKernel_of_isFiniteKernel_fst (h := isFiniteKernel_of_le hκν)
simp_rw [integral_density hκν a (hseq_meas _)]
rw [← ENNReal.toReal_zero]
have h_cont := ENNReal.continuousAt_toReal ENNReal.zero_ne_top
refine h_cont.tendsto.comp ?_
have h : Tendsto (fun m ↦ κ a (univ ×ˢ seq m)) atTop (𝓝 ((κ a) (⋂ n, (fun m ↦ univ ×ˢ seq m) n))) :=
by
apply tendsto_measure_iInter_atTop
· measurability
· exact antitone_const.set_prod hseq
· exact ⟨0, measure_ne_top _ _⟩
simpa [← prod_iInter, hseq_iInter] using h
