English
For a fixed a and s ⊆ β (measurable), the L-integral of the kernel conditioned on (a,b) and restricted to s equals the measure of s×t under κ a for any measurable t.
Русский
Для данного a и измеримого множества s плотностная интеграла ядра при условии (a,b) и ограничении на s равна мере множества s×t под κ a.
LaTeX
$$$\\forall a\\in\\alpha,\\; s\\subseteq\\beta\\text{ измеримо},\\; \\, \\int_{b} \\; \\mathrm{condKernel}_{κ}(a,b)(t) \\, d(κ a)(b) = κ a(s\\times t)$$$
Lean4
theorem tendsto_density_fst_atTop_ae_of_monotone [IsFiniteKernel κ] (a : α) (seq : ℕ → Set β) (hseq : Monotone seq)
(hseq_iUnion : ⋃ i, seq i = univ) (hseq_meas : ∀ m, MeasurableSet (seq m)) :
∀ᵐ x ∂(fst κ a), Tendsto (fun m ↦ density κ (fst κ) a x (seq m)) atTop (𝓝 1) :=
by
refine tendsto_of_integral_tendsto_of_monotone ?_ (integrable_const _) ?_ ?_ ?_
· exact fun m ↦ integrable_density le_rfl _ (hseq_meas m)
· rw [MeasureTheory.integral_const, smul_eq_mul, mul_one]
convert tendsto_integral_density_of_monotone (κ := κ) le_rfl a seq hseq hseq_iUnion hseq_meas
simp only [measureReal_def]
rw [fst_apply' _ _ MeasurableSet.univ]
simp only [mem_univ, setOf_true]
· exact ae_of_all _ (fun c n m hnm ↦ density_mono_set le_rfl a c (hseq hnm))
· exact ae_of_all _ (fun x m ↦ density_le_one le_rfl a x (seq m))
