tendsto_densityProcess_fst_atTop_ae_of_monotone

English

For all α, β, γ with appropriate structure, the equality in the _simp_1_3 block holds, expressing a countable-analytic equivalence of density-related measures along fst and prod decompositions.

Русский

Для всех совместимых структур α, β, γ верно тождество из блока _simp_1_3, выражающее эквивалентность плотностей по разложениям fst и произведение.

LaTeX

$$$\\forall a, \\quad \\text{Eq}\\bigl( \\text{Set.iInter}(\\lambda i, \\operatorname{seq} i) , \\emptyset \\bigr)$$$

Lean4

theorem tendsto_densityProcess_fst_atTop_ae_of_monotone (κ : Kernel α (γ × β)) [IsFiniteKernel κ] (n : ℕ) (a : α)
    (seq : ℕ → Set β) (hseq : Monotone seq) (hseq_iUnion : ⋃ i, seq i = univ) :
    ∀ᵐ x ∂(fst κ a), Tendsto (fun m ↦ densityProcess κ (fst κ) n a x (seq m)) atTop (𝓝 1) :=
  by
  filter_upwards [densityProcess_fst_univ_ae κ n a] with x hx
  rw [← hx]
  exact tendsto_densityProcess_fst_atTop_univ_of_monotone κ n a x seq hseq hseq_iUnion

Похожие утверждения