[Merged by Bors] - feat(measure_theory/function/uniform_integrable): Egorov's theorem

[JasonKYi]

This PR proves Egorov's theorem which is necessary for the Vitali convergence theorem which is vital for the martingale convergence theorems.

---

[RemyDegenne]

You could extract the following lemma from your proof of tendsto_uniformly_on_of_ae_tendsto:

lemma tendsto_uniformly_on_diff_Union_not_convergent_seq
  (hf : ∀ n, measurable (f n)) (hg : measurable g)
  {s : set α} (hsm : measurable_set s) (hs : μ s ≠ ∞)
  (hfg : ∀ᵐ x ∂μ, x ∈ s → tendsto (λ n, f n x) at_top (𝓝 (g x))) {ε : ℝ} (hε : 0 < ε) :
  tendsto_uniformly_on f g at_top (s \ egorov.Union_not_convergent_seq hε hf hg hsm hs hfg) :=
begin
  rw metric.tendsto_uniformly_on_iff,
  intros δ hδ,
  obtain ⟨N, hN⟩ := exists_nat_one_div_lt hδ,
  rw eventually_at_top,
  refine ⟨egorov.not_convergent_seq_lt_index (half_pos hε) hf hg hsm hs hfg N, λ n hn x hx, _⟩,
  simp only [mem_diff, egorov.Union_not_convergent_seq, not_exists, mem_Union, mem_inter_eq,
    not_and, exists_and_distrib_left] at hx,
  obtain ⟨hxs, hx⟩ := hx,
  specialize hx hxs N,
  rw egorov.mem_not_convergent_seq_iff at hx,
  push_neg at hx,
  rw dist_comm,
  exact lt_of_le_of_lt (hx n hn) hN,
end

[RemyDegenne]

Thanks!
bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests