English
Assume f and g are as above with a measurable subset s of finite measure. If f n converge to g almost everywhere on s, then for each n the measure of the set s ∩ notConvergentSeq f g n j tends to 0 as j grows along atTop.
Русский
Пусть f и g удовлетворяют условиям, есть измеримое множество s с конечной мерой. Если f_n сходится почти всюду к g на s, то для каждого n мера множества s ∩ notConvergentSeq f g n j стремится к нулю при j → atTop.
LaTeX
$$$\forall n,\; Tendsto(\lambda j. μ(s \cap notConvergentSeq f g n j))\to 0 \,\text{при } j\to atTop.$$$
Lean4
theorem measure_notConvergentSeq_tendsto_zero [SemilatticeSup ι] [Countable ι] (hf : ∀ n, StronglyMeasurable (f n))
(hg : StronglyMeasurable g) (hsm : MeasurableSet s) (hs : μ s ≠ ∞)
(hfg : ∀ᵐ x ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))) (n : ℕ) :
Tendsto (fun j => μ (s ∩ notConvergentSeq f g n j)) atTop (𝓝 0) :=
by
rcases isEmpty_or_nonempty ι with h | h
· have : (fun j => μ (s ∩ notConvergentSeq f g n j)) = fun j => 0 := by simp only [eq_iff_true_of_subsingleton]
rw [this]
exact tendsto_const_nhds
rw [← measure_inter_notConvergentSeq_eq_zero hfg n, Set.inter_iInter]
refine
tendsto_measure_iInter_atTop (fun n ↦ (hsm.inter <| notConvergentSeq_measurableSet hf hg).nullMeasurableSet)
(fun k l hkl => Set.inter_subset_inter_right _ <| notConvergentSeq_antitone hkl)
⟨h.some, ne_top_of_le_ne_top hs (measure_mono Set.inter_subset_left)⟩
