PrimeNumberTheoremAnd

γ = -Γ'(1) = -∫₀^∞ log(t) exp(-t) dt. -/ theorem eulerMascheroni_eq_neg_integral : eulerMascheroniConstant = -(∫ t in Ioi (0 : ℝ), log t * exp (-t)) := by -- Step 1: Get the complex derivative of GammaIntegral at s = 1 have hpos : (0 : ℝ) < (1 : ℂ).re := by simp have hderiv_integral := Complex.hasDerivAt_GammaIntegral hpos -- Step 2: Gamma = GammaIntegral on {s | 0 < s.re}, which is a nhd of 1 have heq : Complex.Gamma =ᶠ[𝓝 1] Complex.GammaIntegral := by have : {s : ℂ | 0 < s.re} ∈ 𝓝 (1 : ℂ) := by apply IsOpen.mem_nhds · exact isOpen_lt continuous_const Complex.continuous_re · simp exact Filter.eventuallyEq_iff_exists_mem.mpr ⟨{s : ℂ | 0 < s.re}, this, fun s hs => Complex.Gamma_eq_integral hs⟩ -- Step 3: So Gamma has the same derivative as GammaIntegral at 1 have hderiv_Gamma := hderiv_integral.congr_of_eventuallyEq heq -- Step 4: But we also know the derivative of complex Gamma at 1 have hderiv_known := Complex.hasDerivAt_Gamma_one -- Step 5: By uniqueness of derivatives have key := hderiv_Gamma.unique hderiv_known -- Step 6: Simplify the integral in key -- The integrand is ↑t ^ (1 - 1) * (↑(log t) * ↑(rexp (-t))) -- Simplify to ↑(log t * exp(-t)) using t^0 = 1 have simp_integral : (∫ t : ℝ in Ioi 0, (t : ℂ) ^ ((1 : ℂ) - 1) * (↑(log t) * ↑(rexp (-t)))) = ↑(∫ t : ℝ in Ioi 0, log t * rexp (-t)) := by rw [show (1 : ℂ) - 1 = 0 from sub_self 1] simp_rw [Complex.cpow_zero, one_mul, ← Complex.ofReal_mul] exact integral_ofReal rw [simp_integral] at key -- key : ↑(∫ t in Ioi 0, log t * rexp (-t)) = -↑eulerMascheroniConstant rw [← Complex.ofReal_neg] at key have := Complex.ofReal_injective key.symm linarith

namespace FubiniLogExpNeg

/-! ## Integrability lemmas -/

lemma integrableOn_log_Ioc : IntegrableOn log (Set.Ioc 0 1) := (intervalIntegral.intervalIntegrable_log' (a := 0) (b := 1)).1

lemma integrableOn_log_mul_exp_neg_Ioc : IntegrableOn (fun t => log t * exp (-t)) (Set.Ioc 0 1) := integrableOn_log_Ioc.mul_continuousOn_of_subset (continuous_exp.comp continuous_neg).continuousOn measurableSet_Ioc isCompact_Icc Ioc_subset_Icc_self

lemma integrableOn_log_mul_exp_neg_Ioi_one : IntegrableOn (fun t => log t * exp (-t)) (Set.Ioi 1) := by have hg : IntegrableOn (fun t => t * exp (-t)) (Set.Ioi 1) := by have := (GammaIntegral_convergent (s := 2) (by norm_num : (0 : ℝ) < 2)).mono_set (Set.Ioi_subset_Ioi zero_le_one) apply this.congr filter_upwards [self_mem_ae_restrict measurableSet_Ioi] with t ht simp only [Set.mem_Ioi] at ht rw [show (2 : ℝ) - 1 = 1 from by norm_num, rpow_one t, mul_comm] rw [IntegrableOn] at hg ⊢ exact hg.mono ((measurable_log.mul (continuous_exp.comp continuous_neg).measurable).aestronglyMeasurable.restrict) (by filter_upwards [self_mem_ae_restrict measurableSet_Ioi] with t ht simp only [Set.mem_Ioi] at ht have ht0 : (0 : ℝ) < t := lt_trans zero_lt_one ht rw [norm_mul, norm_mul, Real.norm_eq_abs (log t), Real.norm_eq_abs t, abs_of_nonneg (log_nonneg ht.le), abs_of_pos ht0] exact mul_le_mul_of_nonneg_right (log_le_self ht0.le) (norm_nonneg _))

lemma integrableOn_exp_neg_div_Ioi_one : IntegrableOn (fun t => exp (-t) / t) (Set.Ioi 1) := by have hg : IntegrableOn (fun t => exp (-t)) (Set.Ioi 1) := by have := (GammaIntegral_convergent (s := 1) (by norm_num : (0 : ℝ) < 1)).mono_set (Set.Ioi_subset_Ioi zero_le_one) apply this.congr filter_upwards [self_mem_ae_restrict measurableSet_Ioi] with t ht simp only [Set.mem_Ioi] at ht rw [show (1 : ℝ) - 1 = 0 from by norm_num, rpow_zero, mul_one] rw [IntegrableOn] at hg ⊢ exact hg.mono ((continuous_exp.comp continuous_neg).measurable.div measurable_id).aestronglyMeasurable.restrict (by filter_upwards [self_mem_ae_restrict measurableSet_Ioi] with t ht simp only [Set.mem_Ioi] at ht have ht0 : (0 : ℝ) < t := lt_trans zero_lt_one ht rw [norm_div, Real.norm_eq_abs, Real.norm_eq_abs, abs_of_pos (exp_pos _), abs_of_pos ht0] exact div_le_self (le_of_lt (exp_pos _)) (le_of_lt ht))

/-! ## IBP on (1, ∞): ∫₁^∞ log(t) exp(-t) dt = ∫₁^∞ exp(-t)/t dt

For a > 1, the substitution t = eᵘ transforms ∫ₐᵇ dt/log(t) into ∫_{log a}^{log b} eᵘ/u du.