pv_exp_div_eq_gamma_add_log_add_integral

theorem pv_exp_div_eq_gamma_add_log_add_integral {y : ℝ} (hy : 0 < y) :    lim ((𝓝[>] (0 : ℝ)).map (fun ε =>      (∫ u in (-1/ε)..(-ε), exp u / u) + ∫ u in ε..y, exp u / u)) =    eulerMascheroniConstant + log y + ∫ u in (0 : ℝ)..y, ((exp u - 1) / u) := by  -- Suffices to show Tendsto  apply lim_eq  -- Rewrite the target  rw [show eulerMascheroniConstant + log y + ∫ u in (0 : ℝ)..y, ((exp u - 1) / u) =    ((∫ t in (0:ℝ)..1, (1 - exp (-t)) / t) - ∫ t in Ioi (1:ℝ), exp (-t) / t) +    (∫ u in (0:ℝ)..y, (exp u - 1) / u) + log y by      rw [← eulerMascheroni_eq_integral]; ring]  -- The rewritten form converges  have h_rw : Tendsto    (fun ε => (∫ t in ε..1, (1 - exp (-t)) / t) - (∫ t in (1:ℝ)..(1/ε), exp (-t) / t) +      (∫ u in ε..y, (exp u - 1) / u) + log y)    (𝓝[>] (0 : ℝ))    (𝓝 (((∫ t in (0:ℝ)..1, (1 - exp (-t)) / t) - ∫ t in Ioi (1:ℝ), exp (-t) / t) +      (∫ u in (0:ℝ)..y, (exp u - 1) / u) + log y)) := by    exact ((tendsto_integral_one_sub_exp_neg_div.sub tendsto_integral_exp_neg_div_Ioi).add      (tendsto_integral_exp_sub_one_div hy)).add tendsto_const_nhds  -- Show the original function is eventually equal to the rewritten form  apply h_rw.congr'  have : ∀ᶠ ε in 𝓝[>] (0 : ℝ), ε < min y 1 := by    apply nhdsWithin_le_nhds    exact Iio_mem_nhds (lt_min hy one_pos)  filter_upwards [this, self_mem_nhdsWithin] with ε hε hε_pos  exact (pv_rewrite hy hε_pos (lt_of_lt_of_le hε (min_le_right _ _))    (lt_of_lt_of_le hε (min_le_left _ _))).symm