English
Another monotone convergence variant: with union univ and measurable seq m, the limit of integrals equals the integral over univ.
Русский
Ещё одно вариация монотонной сходимости: с объединением univ и измеримыми seq m предел интегралов равен интегралу по univ.
LaTeX
$$Eq (Set.iUnion fun i => seq i) Set.univ$$
Lean4
theorem tendsto_integral_density_of_monotone (hκν : fst κ ≤ ν) [IsFiniteKernel ν] (a : α) (seq : ℕ → Set β)
(hseq : Monotone seq) (hseq_iUnion : ⋃ i, seq i = univ) (hseq_meas : ∀ m, MeasurableSet (seq m)) :
Tendsto (fun m ↦ ∫ x, density κ ν a x (seq m) ∂(ν a)) atTop (𝓝 ((κ a).real univ)) :=
by
have : IsFiniteKernel κ := isFiniteKernel_of_isFiniteKernel_fst (h := isFiniteKernel_of_le hκν)
simp_rw [integral_density hκν a (hseq_meas _)]
have h_cont := ENNReal.continuousOn_toReal.continuousAt (x := κ a univ) ?_
swap
· rw [mem_nhds_iff]
refine ⟨Iio (κ a univ + 1), fun x hx ↦ ne_top_of_lt (?_ : x < κ a univ + 1), isOpen_Iio, ?_⟩
· simpa using hx
· simp only [mem_Iio]
exact ENNReal.lt_add_right (measure_ne_top _ _) one_ne_zero
refine h_cont.tendsto.comp ?_
convert tendsto_measure_iUnion_atTop (monotone_const.set_prod hseq)
rw [← prod_iUnion, hseq_iUnion, univ_prod_univ]
