tendsto_zero_of_antitone — Mathlib

English

If seq is antitone in ℚ and tends to 0, then for a.e. c, the sequence f(a,c)(seq m) tends to 0 in ℝ.

Русский

Если последовательность в ℚ антимонотонна и стремится к 0, то для а.е. c последовательность f(a,c)(seq m) сходится к 0.

LaTeX

$$$\text{ae}_{c\sim ν(a)}(\text{Tendsto}(n\mapsto f(a,c)(seq(n)))\;\text{atTop}\; 0)\text{ при антимонотонности seq}.$$$

Lean4

theorem tendsto_zero_of_antitone (hf : IsRatCondKernelCDFAux f κ ν) [IsFiniteKernel ν] (a : α) (seq : ℕ → ℚ)
    (hseq : Antitone seq) (hseq_tendsto : Tendsto seq atTop atBot) :
    ∀ᵐ c ∂(ν a), Tendsto (fun m ↦ f (a, c) (seq m)) atTop (𝓝 0) :=
  by
  refine tendsto_of_integral_tendsto_of_antitone ?_ (integrable_const _) ?_ ?_ ?_
  · exact fun n ↦ hf.integrable a (seq n)
  · rw [integral_zero]
    exact hf.tendsto_integral_of_antitone a seq hseq hseq_tendsto
  · filter_upwards [hf.mono a] with t ht using fun n m hnm ↦ ht (hseq hnm)
  · filter_upwards [hf.nonneg a] with c hc using fun i ↦ hc (seq i)

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