LiSeries.integral_exp_sub_one_div_eq_tsum

theorem integral_exp_sub_one_div_eq_tsum (y : ℝ) :    ∫ u in (0 : ℝ)..y, ((exp u - 1) / u) =      ∑' n : ℕ, y ^ (n + 1) / ((↑(n + 1) : ℝ) * ↑(n + 1).factorial) := by  -- Step 1: Swap ∫ and ∑ using summability of norms  have hswap := intervalIntegral.tsum_intervalIntegral_eq_of_summable_norm    (summable_termFun_norm 0 y)  simp only [show ∀ n, (fun x => (termFun n) x) = fun u => u ^ n / ↑(n + 1).factorial from    fun n => rfl] at hswap  -- Step 2: Compute each integral  simp_rw [integral_term] at hswap  -- hswap: ∑' n, y^{n+1}/((n+1)*(n+1)!) = ∫₀ʸ ∑' n, u^n/(n+1)!  -- Step 3: Show ∫₀ʸ (exp u - 1)/u = ∫₀ʸ ∑' n, u^n/(n+1)! (they agree a.e.)  trans (∫ u in (0 : ℝ)..y, ∑' n : ℕ, u ^ n / ↑(n + 1).factorial)  · apply intervalIntegral.integral_congr_ae    -- (exp u - 1)/u = ∑ u^n/(n+1)! for u ≠ 0 by hasSum_exp_sub_one_div;    -- {0} has Lebesgue measure zero, so the equality holds a.e.    have hae : ∀ᵐ (u : ℝ), u ≠ 0 :=      ae_iff.mpr (by simp [show (volume : Measure ℝ) {(0 : ℝ)} = 0 from by simp])    exact hae.mono (fun u hu _ => (hasSum_exp_sub_one_div hu).tsum_eq.symm)  · exact hswap.symm