tendstoInMeasure_iff_enorm — Mathlib

English

An equivalent formulation of TendstoInMeasure using ENNReal norm, with equivalence to norms via edist.

Русский

Эквивалентная формулировка TendstoInMeasure через ENNReal норму, используя edist.

LaTeX

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

Lean4

theorem tendstoInMeasure_iff_enorm [SeminormedAddCommGroup E] {l : Filter ι} {f : ι → α → E} {g : α → E} :
    TendstoInMeasure μ f l g ↔ ∀ ε, 0 < ε → ε ≠ ∞ → Tendsto (fun i => μ {x | ε ≤ ‖f i x - g x‖ₑ}) l (𝓝 0) :=
  by
  simp_rw [← edist_eq_enorm_sub]
  exact ⟨fun h ε hε hε_top ↦ h ε hε, tendstoInMeasure_of_ne_top⟩

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