tendsto_one_of_monotone — Mathlib

English

If seq is monotone and tends to +∞, then a.e. c, f(a,c)(seq m) tends to 1.

Русский

Пусть seq монотонна и стремится к +∞; тогда для почти всех c выполняется сходящаяся к 1 последовательность f(a,c)(seq m).

LaTeX

$$$\text{ae}_{c\sim ν(a)}(\text{Tendsto}(m\mapsto f(a,c)(seq(m)))\;\text{atTop}\; 1).$$$

Lean4

theorem tendsto_one_of_monotone (hf : IsRatCondKernelCDFAux f κ ν) [IsFiniteKernel ν] (a : α) (seq : ℕ → ℚ)
    (hseq : Monotone seq) (hseq_tendsto : Tendsto seq atTop atTop) :
    ∀ᵐ c ∂(ν a), Tendsto (fun m ↦ f (a, c) (seq m)) atTop (𝓝 1) :=
  by
  refine tendsto_of_integral_tendsto_of_monotone ?_ (integrable_const _) ?_ ?_ ?_
  · exact fun n ↦ hf.integrable a (seq n)
  · rw [MeasureTheory.integral_const, smul_eq_mul, mul_one]
    exact hf.tendsto_integral_of_monotone a seq hseq hseq_tendsto
  · filter_upwards [hf.mono a] with t ht using fun n m hnm ↦ ht (hseq hnm)
  · filter_upwards [hf.le_one a] with c hc using fun i ↦ hc (seq i)

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