Uniform Integrable iff tendsto i Sup e Lp Norm indicator norm

lemma uniformIntegrable_iff_tendsto_iSup_eLpNorm_indicator_norm [IsFiniteMeasure μ]    [NormedAddCommGroup E] {X : κ → Ω → E} (hX : ∀ k, AEStronglyMeasurable (X k) μ) :    UniformIntegrable X 1 μ ↔      Tendsto (fun c : ℝ≥0 =>        ⨆ k, eLpNorm ({ω | c < ‖X k ω‖₊}.indicator (X k)) 1 μ) atTop (𝓝 0) := by  let tail : ℝ≥0 → ℝ≥0∞ := fun c ↦ ⨆ i : κ, eLpNorm ({ω | c < ‖X i ω‖₊}.indicator (X i)) 1 μ  -- We first show that this tail function is antitone so that convergence at `atTop` can be checked  -- by `ENNReal.tendsto_atTop_zero_iff_le_of_antitone htail_mono`.  have htail_anti : Antitone tail := by    refine fun c d hcd => iSup_mono fun k => eLpNorm_mono_enorm fun ω => ?_    by_cases hω : d < ‖X k ω‖₊    · simp [hω, hcd.trans_lt hω]    · simp [hω]  rw [uniformIntegrable_iff' (refl 1) ENNReal.one_ne_top]  refine ⟨fun ⟨_, htail⟩ => ?_, fun htail => ⟨hX, fun ε hε => ?_⟩⟩  · refine (ENNReal.tendsto_atTop_zero_iff_le_of_antitone htail_anti).2 fun ε hε => ?_    by_cases hε_top : ε = ∞    · exact ⟨0, by simp [hε_top]⟩    · have hε_real_pos : 0 < ε.toReal := ENNReal.toReal_pos hε.ne' hε_top      obtain ⟨C, hC⟩ := htail ε.toReal hε_real_pos      exact ⟨C, iSup_le_iff.2 fun i => (hC i).trans_eq (ENNReal.ofReal_toReal hε_top)⟩  · rw [ENNReal.tendsto_atTop_zero_iff_le_of_antitone htail_anti] at htail    obtain ⟨C, hC⟩ := htail (ENNReal.ofReal ε) (ENNReal.ofReal_pos.2 hε)    exact ⟨C, fun i => (le_iSup _ i).trans hC⟩