English
From TendstoInMeasure, obtain a subsequence ns and a further subsequence ns' witnessing almost-everywhere convergence for f under g.
Русский
Из TendstoInMeasure получить подпоследовательность ns и еще подпоследовательность ns', демонстрирующие почти везде сходимость для f относительно g.
LaTeX
$$$\exists ns: \mathbb{N}\to \mathbb{N},\;\exists ns':\mathbb{N}\to \mathbb{N},\; Tendsto ns\ atTop u \wedge TendstoInMeasure(\mu, f\circ ns, atTop, g) \wedge \forall^{ae} x,\; Tendsto (f(ns(n)))(x)\to g(x).$$$
Lean4
/-- `TendstoInMeasure` is equivalent to every subsequence having another subsequence
which converges almost surely. -/
theorem exists_seq_tendstoInMeasure_atTop_iff [IsFiniteMeasure μ] {f : ℕ → α → E}
(hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ) {g : α → E} :
TendstoInMeasure μ f atTop g ↔
∀ ns : ℕ → ℕ,
StrictMono ns →
∃ ns' : ℕ → ℕ, StrictMono ns' ∧ ∀ᵐ (ω : α) ∂μ, Tendsto (fun i ↦ f (ns (ns' i)) ω) atTop (𝓝 (g ω)) :=
by
refine ⟨fun hfg _ hns ↦ (hfg.comp hns.tendsto_atTop).exists_seq_tendsto_ae, not_imp_not.mp (fun h1 ↦ ?_)⟩
rw [tendstoInMeasure_iff_tendsto_toNNReal] at h1
push_neg at *
obtain ⟨ε, hε, h2⟩ := h1
obtain ⟨δ, ns, hδ, hns, h3⟩ :
∃ (δ : ℝ≥0) (ns : ℕ → ℕ), 0 < δ ∧ StrictMono ns ∧ ∀ n, δ ≤ (μ {x | ε ≤ edist (f (ns n) x) (g x)}).toNNReal :=
by
obtain ⟨s, hs, h4⟩ := not_tendsto_iff_exists_frequently_notMem.1 h2
obtain ⟨δ, hδ, h5⟩ := NNReal.nhds_zero_basis.mem_iff.1 hs
obtain ⟨ns, hns, h6⟩ := extraction_of_frequently_atTop h4
exact ⟨δ, ns, hδ, hns, fun n ↦ Set.notMem_Iio.1 (Set.notMem_subset h5 (h6 n))⟩
refine ⟨ns, hns, fun ns' _ ↦ ?_⟩
by_contra h6
have h7 := tendstoInMeasure_iff_tendsto_toNNReal.mp <| tendstoInMeasure_of_tendsto_ae (fun n ↦ hf _) h6
exact lt_irrefl _ (lt_of_le_of_lt (ge_of_tendsto' (h7 ε hε) (fun n ↦ h3 _)) hδ)
