English
Equivalence between TendstoInMeasure and a dist-based formulation: with dist in place of edist.
Русский
Эквивалентность между TendstoInMeasure и формулировкой по расстоянию: вместо edist берём dist.
LaTeX
$$$TendstoInMeasure μ f l g \\iff \\forall ε>0, Tendsto (i ↦ μ\\{x| ε≤ dist(f_i x,g x)\\}) l (𝓝 0)$$$
Lean4
theorem tendstoInMeasure_iff_dist [PseudoMetricSpace E] {f : ι → α → E} {l : Filter ι} {g : α → E} :
TendstoInMeasure μ f l g ↔ ∀ ε, 0 < ε → Tendsto (fun i => μ {x | ε ≤ dist (f i x) (g x)}) l (𝓝 0) :=
by
refine ⟨fun h ε hε ↦ ?_, fun h ↦ ?_⟩
· convert h (ENNReal.ofReal ε) (ENNReal.ofReal_pos.mpr hε) with i a
rw [edist_dist, ENNReal.ofReal_le_ofReal_iff (by positivity)]
· refine tendstoInMeasure_of_ne_top fun ε hε hε_top ↦ ?_
convert h ε.toReal (ENNReal.toReal_pos hε.ne' hε_top) with i a
rw [edist_dist, ENNReal.le_ofReal_iff_toReal_le hε_top (by positivity)]
