tendsto_densityProcess_atTop_of_antitone

English

If seq is antitone with empty intersection, then densityProcess κ ν n a x (seq m) tends to 0 as m grows.

Русский

Если seq антитонична и пересечениеSeq равняется пустому множеству, то densityProcess κ ν n a x (seq m) стремится к 0 при росте m.

LaTeX

$$$\displaystyle \lim_{m\to\infty} \densityProcess κ ν n a x (seq m) = 0$$$

Lean4

theorem tendsto_densityProcess_atTop_of_antitone (κ : Kernel α (γ × β)) (ν : Kernel α γ) [IsFiniteKernel κ] (n : ℕ)
    (a : α) (x : γ) (seq : ℕ → Set β) (hseq : Antitone seq) (hseq_iInter : ⋂ i, seq i = ∅)
    (hseq_meas : ∀ m, MeasurableSet (seq m)) : Tendsto (fun m ↦ densityProcess κ ν n a x (seq m)) atTop (𝓝 0) :=
  by
  rw [← densityProcess_empty κ ν n a x]
  exact tendsto_densityProcess_atTop_empty_of_antitone κ ν n a x seq hseq hseq_iInter hseq_meas

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