tendstoInMeasure_of_ne_top — Mathlib

English

Under finite-measure assumptions, TendstoInMeasure is equivalent to Tendsto to NNReal of the quantities μ{x|ε≤edist...}.

Русский

При конечной мере эквивалентно движение TendstoInMeasure к Tendsto к NNReal для выражения μ{x|ε≤edist...}.

LaTeX

$$$TendstoInMeasure μ f l g \\iff \\forall ε>0, Tendsto (i ↦ μ\\{x| ε≤edist (f_i x)(g x)\\}) l (𝓝 0)$$$

Lean4

theorem tendstoInMeasure_of_ne_top [EDist E] {f : ι → α → E} {l : Filter ι} {g : α → E}
    (h : ∀ ε, 0 < ε → ε ≠ ∞ → Tendsto (fun i => μ {x | ε ≤ edist (f i x) (g x)}) l (𝓝 0)) : TendstoInMeasure μ f l g :=
  by
  intro ε hε
  by_cases hε_top : ε = ∞
  · have h1 : Tendsto (fun n ↦ μ {ω | 1 ≤ edist (f n ω) (g ω)}) l (𝓝 0) := h 1 (by simp) (by simp)
    refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds h1 (fun _ ↦ zero_le') ?_
    intro n
    simp only [hε_top]
    gcongr
    simp
  · exact h ε hε hε_top

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