English
There exists a subsequence ns such that ns is strictly increasing and f(ns(i))(x) tends to g(x) a.e. for μ-almost every x.
Русский
Существует подпоследовательность ns, такая что ns строго возрастает и f(ns(i))(x) сходится к g(x) почти на μ- almost-everywhere.
LaTeX
$$$\exists ns: \mathbb{N}\to\mathbb{N},\; StrictMono(ns) \wedge \forall^{\mathrm{ae}} x, \, Tendsto (\lambda i, f(ns(i))(x)) atTop (\mathcal{N}(g(x))).$$$
Lean4
/-- If `f` is a sequence of functions which converges in measure to `g`, then there exists a
subsequence of `f` which converges a.e. to `g`. -/
theorem exists_seq_tendsto_ae (hfg : TendstoInMeasure μ f atTop g) :
∃ ns : ℕ → ℕ, StrictMono ns ∧ ∀ᵐ x ∂μ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x)) := by
/- Since `f` tends to `g` in measure, it has a subsequence `k ↦ f (ns k)` such that
`μ {|f (ns k) - g| ≥ 2⁻ᵏ} ≤ 2⁻ᵏ` for all `k`. Defining
`s := ⋂ k, ⋃ i ≥ k, {|f (ns k) - g| ≥ 2⁻ᵏ}`, we see that `μ s = 0` by the
first Borel-Cantelli lemma.
On the other hand, as `s` is precisely the set for which `f (ns k)`
doesn't converge to `g`, `f (ns k)` converges almost everywhere to `g` as required. -/
have h_lt_ε_real (ε : ℝ≥0∞) (hε : 0 < ε) : ∃ k : ℕ, 2 * (2 : ℝ≥0∞)⁻¹ ^ k < ε :=
by
obtain ⟨k, h_k⟩ : ∃ k : ℕ, (2 : ℝ≥0∞)⁻¹ ^ k < ε := ENNReal.exists_inv_two_pow_lt hε.ne'
refine ⟨k + 1, lt_of_eq_of_lt ?_ h_k⟩
rw [pow_succ', ← mul_assoc, ENNReal.mul_inv_cancel, one_mul]
· positivity
· simp
set ns := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
use ns
let S := fun k => {x | (2 : ℝ≥0∞)⁻¹ ^ k ≤ edist (f (ns k) x) (g x)}
have hμS_le : ∀ k, μ (S k) ≤ (2 : ℝ≥0∞)⁻¹ ^ k := fun k => ExistsSeqTendstoAe.seqTendstoAeSeq_spec hfg k (ns k) le_rfl
set s := Filter.atTop.limsup S with hs
have hμs : μ s = 0 :=
by
refine measure_limsup_atTop_eq_zero (ne_top_of_le_ne_top ?_ (ENNReal.tsum_le_tsum hμS_le))
simpa only [ENNReal.tsum_geometric, ENNReal.one_sub_inv_two, inv_inv] using ENNReal.ofNat_ne_top
have h_tendsto : ∀ x ∈ sᶜ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x)) :=
by
refine fun x hx => EMetric.tendsto_atTop.mpr fun ε hε => ?_
rw [hs, limsup_eq_iInf_iSup_of_nat] at hx
simp only [S, Set.iSup_eq_iUnion, Set.iInf_eq_iInter, Set.compl_iInter, Set.compl_iUnion, Set.mem_iUnion,
Set.mem_iInter, Set.mem_compl_iff, Set.mem_setOf_eq, not_le] at hx
obtain ⟨N, hNx⟩ := hx
obtain ⟨k, hk_lt_ε⟩ := h_lt_ε_real ε hε
refine ⟨max N (k - 1), fun n hn_ge => lt_of_le_of_lt ?_ hk_lt_ε⟩
specialize hNx n ((le_max_left _ _).trans hn_ge)
have h_inv_n_le_k : (2 : ℝ≥0∞)⁻¹ ^ n ≤ 2 * (2 : ℝ≥0∞)⁻¹ ^ k :=
by
nth_rw 2 [← pow_one (2 : ℝ≥0∞)]
rw [mul_comm, ← ENNReal.inv_pow, ← ENNReal.inv_pow, ENNReal.inv_le_iff_le_mul, ← mul_assoc, mul_comm (_ ^ n),
mul_assoc, ← ENNReal.inv_le_iff_le_mul, inv_inv, ← pow_add]
· gcongr
· simp
· omega
all_goals simp
exact le_trans hNx.le h_inv_n_le_k
rw [ae_iff]
refine ⟨ExistsSeqTendstoAe.seqTendstoAeSeq_strictMono hfg, measure_mono_null (fun x => ?_) hμs⟩
rw [Set.mem_setOf_eq, ← @Classical.not_not (x ∈ s), not_imp_not]
exact h_tendsto x
