LiSeries.FubiniLogExpNeg.ibp_Ioi_one
PrimeNumberTheoremAnd.IEANTN.LiSeries · PrimeNumberTheoremAnd/IEANTN/LiSeries.lean:234 to 272
Source documentation
γ = -Γ'(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
Exact Lean statement
lemma ibp_Ioi_one :
∫ t in Set.Ioi (1 : ℝ), log t * exp (-t) =
∫ t in Set.Ioi (1 : ℝ), exp (-t) / tComplete declaration
Lean source
lemma ibp_Ioi_one : ∫ t in Set.Ioi (1 : ℝ), log t * exp (-t) = ∫ t in Set.Ioi (1 : ℝ), exp (-t) / t := by have hlog_deriv : ∀ t ∈ Set.Ioi (1 : ℝ), HasDerivAt log (t⁻¹) t := fun t ht => Real.hasDerivAt_log (ne_of_gt (lt_trans one_pos ht)) have hv_deriv : ∀ t ∈ Set.Ioi (1 : ℝ), HasDerivAt (fun t => -exp (-t)) (exp (-t)) t := by intro t _; have h := (hasDerivAt_neg t).exp.neg; convert! h using 1; simp [mul_comm] have h_uv'_int : IntegrableOn (log * fun t => exp (-t)) (Set.Ioi 1) := integrableOn_log_mul_exp_neg_Ioi_one have h_u'v_int : IntegrableOn ((fun t => t⁻¹) * fun t => -exp (-t)) (Set.Ioi 1) := by have := integrableOn_exp_neg_div_Ioi_one.neg refine this.congr ?_ filter_upwards [ae_restrict_mem measurableSet_Ioi] with t _ simp [Pi.mul_apply, div_eq_mul_inv]; ring have h_lim_1 : Tendsto (log * fun t => -exp (-t)) (𝓝[>] (1 : ℝ)) (𝓝 (log 1 * -exp (-(1 : ℝ)))) := by apply Filter.Tendsto.mul · exact (Real.continuousAt_log (by norm_num : (1 : ℝ) ≠ 0)).tendsto.mono_left nhdsWithin_le_nhds · exact ((continuous_exp.comp continuous_neg).neg.continuousAt).tendsto.mono_left nhdsWithin_le_nhds have h_lim_inf : Tendsto (log * fun t => -exp (-t)) atTop (𝓝 0) := by have h1 : Tendsto (fun t : ℝ => t * exp (-t)) atTop (𝓝 0) := by simpa using tendsto_pow_mul_exp_neg_atTop_nhds_zero 1 have h2 : Tendsto (fun t : ℝ => log t * exp (-t)) atTop (𝓝 0) := by apply squeeze_zero_norm' _ h1 filter_upwards [Filter.eventually_ge_atTop (1 : ℝ)] with t ht rw [norm_mul, Real.norm_of_nonneg (Real.log_nonneg ht), Real.norm_of_nonneg (exp_pos _).le] exact mul_le_mul_of_nonneg_right (Real.log_le_self (by linarith)) (exp_pos _).le show Tendsto (fun t : ℝ => log t * (-exp (-t))) atTop (𝓝 0) have h3 := (neg_zero (G := ℝ)) ▸ h2.neg exact Filter.Tendsto.congr (fun t => by ring) h3 rw [integral_Ioi_mul_deriv_eq_deriv_mul hlog_deriv hv_deriv h_uv'_int h_u'v_int h_lim_1 h_lim_inf] simp only [log_one, zero_mul, sub_zero, zero_sub] rw [neg_eq_iff_eq_neg, ← integral_neg] exact setIntegral_congr_fun measurableSet_Ioi (fun t ht => by simp only [Set.mem_Ioi] at ht; simp [div_eq_mul_inv]; ring)