English
If IsFiniteMeasure μ, TendstoInMeasure is equivalent to Tendsto to NNReal of the measures μ{ε≤edist(...)}.
Русский
При конечной мере μ эквивалентно TendstoInMeasure к Tendsto к NNReal для выражения μ{ε≤edist...}.
LaTeX
$$$TendstoInMeasure μ f l g \\iff ∀ ε>0, Tendsto (i ↦ (μ{ x| ε≤edist (f i x) (g x) }).toNNReal) l (𝓝 0)$$$
Lean4
theorem tendstoInMeasure_iff_tendsto_toNNReal [EDist E] [IsFiniteMeasure μ] {f : ι → α → E} {l : Filter ι} {g : α → E} :
TendstoInMeasure μ f l g ↔ ∀ ε, 0 < ε → Tendsto (fun i => (μ {x | ε ≤ edist (f i x) (g x)}).toNNReal) l (𝓝 0) :=
by
have hfin ε i : μ {x | ε ≤ edist (f i x) (g x)} ≠ ⊤ := measure_ne_top μ {x | ε ≤ edist (f i x) (g x)}
refine ⟨fun h ε hε ↦ ?_, fun h ε hε ↦ ?_⟩
· have hf :
(fun i => (μ {x | ε ≤ edist (f i x) (g x)}).toNNReal) =
ENNReal.toNNReal ∘ (fun i ↦ (μ {x | ε ≤ edist (f i x) (g x)})) :=
rfl
rw [hf, ENNReal.tendsto_toNNReal_iff' (hfin ε)]
exact h ε hε
· rw [← ENNReal.tendsto_toNNReal_iff ENNReal.zero_ne_top (hfin ε)]
exact h ε hε
