English
For a finite measure μ and a fixed n, the measure of the intersection of s with all notConvergentSeq sets is zero, under mild almost-everywhere convergence assumptions.
Русский
Для конечной меры μ и фиксированного n мера пересечения множества s с множеством notConvergentSeq по мере нулю, при условии а.e. сходимости.
LaTeX
$$$\mu\bigl(s \cap \bigcap_{j} notConvergentSeq(f,g,n,j)\bigr) = 0$$$
Lean4
theorem measure_inter_notConvergentSeq_eq_zero [SemilatticeSup ι] [Nonempty ι]
(hfg : ∀ᵐ x ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))) (n : ℕ) :
μ (s ∩ ⋂ j, notConvergentSeq f g n j) = 0 :=
by
simp_rw [EMetric.tendsto_atTop, ae_iff] at hfg
rw [← nonpos_iff_eq_zero, ← hfg]
refine measure_mono fun x => ?_
simp only [Set.mem_inter_iff, Set.mem_iInter, mem_notConvergentSeq_iff]
push_neg
rintro ⟨hmem, hx⟩
refine ⟨hmem, (n : ℝ≥0∞)⁻¹, by simp, fun N => ?_⟩
obtain ⟨n, hn₁, hn₂⟩ := hx N
exact ⟨n, hn₁, hn₂.le⟩
