English
Under the same hypotheses as above, for almost every x with respect to ν a, the densities converge to 0 along the antitone sequence seq.
Русский
При тех же условиях для почти всех x относительно меры ν a плотности по последовательности seq сходятся к нулю.
LaTeX
$$$\\forall x\\,\\Big( x \\sim (\\nu a) \\Big),\\; \\operatorname{Tendsto}\\bigl( m \\mapsto \\density_{\\kappa,\\nu}(a,x)(\\mathrm{seq}(m)) \\bigr)\\_{\\operatorname{atTop}} (\\mathcal{N}(0))$$$
Lean4
theorem tendsto_density_atTop_ae_of_antitone (hκν : fst κ ≤ ν) [IsFiniteKernel ν] (a : α) (seq : ℕ → Set β)
(hseq : Antitone seq) (hseq_iInter : ⋂ i, seq i = ∅) (hseq_meas : ∀ m, MeasurableSet (seq m)) :
∀ᵐ x ∂(ν a), Tendsto (fun m ↦ density κ ν a x (seq m)) atTop (𝓝 0) :=
by
refine tendsto_of_integral_tendsto_of_antitone ?_ (integrable_const _) ?_ ?_ ?_
· exact fun m ↦ integrable_density hκν _ (hseq_meas m)
· rw [integral_zero]
exact tendsto_integral_density_of_antitone hκν a seq hseq hseq_iInter hseq_meas
· exact ae_of_all _ (fun c n m hnm ↦ density_mono_set hκν a c (hseq hnm))
· exact ae_of_all _ (fun x m ↦ density_nonneg hκν a x (seq m))
