The Stirling series for the gamma function

Derivatives of y ↦ log (x + y)

theorem contDiffAt_log_add {x y : ℝ} (xy : 0 < x + y) : ContDiffAt ℝ ⊤ (fun (y : ℝ) => Real.log (x + y)) y

theorem contDiffOn_log_add {x : ℝ} {s : WithTop ℕ∞} : ContDiffOn ℝ s (fun (y : ℝ) => Real.log (x + y)) (Set.Ioi (-x))

theorem deriv_log_add {x y : ℝ} (xy : 0 < x + y) : deriv (fun (y : ℝ) => Real.log (x + y)) y = (x + y)⁻¹

theorem HasDerivAt.zpow {x : ℝ} {f : ℝ → ℝ} {f' : ℝ} (df : HasDerivAt f f' x) {n : ℤ} (g : f x ≠ 0 ∨ 0 ≤ n) : HasDerivAt (fun (x : ℝ) => f x ^ n) (↑n * f x ^ (n - 1) * f') x

theorem iteratedDeriv_log_add {x y : ℝ} (xy : 0 < x + y) (s : ℕ) : iteratedDeriv (s + 1) (fun (y : ℝ) => Real.log (x + y)) y = (-1) ^ s * ↑s.factorial * (x + y) ^ (-↑s - 1)

@[simp]

theorem iteratedDerivWithin_log_add_succ {x y : ℝ} (s : ℕ) (xy : 0 < x + y) : iteratedDerivWithin (s + 1) (fun (y : ℝ) => Real.log (x + y)) (Set.Ioi (-x)) y = (-1) ^ s * ↑s.factorial * (x + y) ^ (-↑s - 1)

@[simp]

theorem iteratedDerivWithin_log_add_one {x y : ℝ} (xy : 0 < x + y) : iteratedDerivWithin 1 (fun (y : ℝ) => Real.log (x + y)) (Set.Ioi (-x)) y = (x + y)⁻¹

Rising log factorials and logGammaSeq

def log_rising (x : ℝ) (n : ℕ) : ℝ

log x + log (x + 1) + ... + log (x + n)

Equations

• log_rising x n = 2⁻¹ * (Real.log x + Real.log (x + ↑n)) + trapezoid_sum (fun (k : ℝ) => Real.log (x + k)) 0 n

@[simp]

theorem log_rising_zero (x : ℝ) : log_rising x 0 = Real.log x

theorem log_rising_succ (x : ℝ) (n : ℕ) : log_rising x (n + 1) = log_rising x n + Real.log (x + ↑n + 1)

theorem log_rising_eq_sum (x : ℝ) (n : ℕ) : log_rising x n = ∑ m ∈ Finset.range (n + 1), Real.log (x + ↑m)

theorem log_factorial_eq_log_rising (n : ℕ) : Real.log ↑n.factorial = log_rising 1 (n - 1)

theorem logGammaSeq_eq_rising (x : ℝ) (n : ℕ) : Real.BohrMollerup.logGammaSeq x n = x * Real.log ↑n + log_rising 1 (n - 1) - log_rising x n

Approximating log_rising and gamma via Euler-Maclaurin

def term (x : ℝ) (s : ℕ) : ℝ

Equations

• term x s = ↑(bernoulli (s + 2)) / ((↑s + 1) * (↑s + 2)) / x ^ (s + 1)

def sum (x : ℝ) (s : ℕ) : ℝ

Equations

• sum x s = ∑ m ∈ Finset.range (s + 1), term x m

def rem_n (x : ℝ) (n s : ℕ) : ℝ

Equations

• rem_n x n s = ↑(s + 1).factorial * ∫ (t : ℝ) in 0..↑n, saw (s + 2) t / (x + t) ^ (s + 2)

def rem (x : ℝ) (s : ℕ) : ℝ

Equations

• rem x s = ↑(s + 1).factorial * ∫ (t : ℝ) in Set.Ioi 0, saw (s + 2) t / (x + t) ^ (s + 2)

def pre_n (x : ℝ) (n : ℕ) : ℝ

Equations

• pre_n x n = (x + ↑n + 2⁻¹) * Real.log (↑n / (x + ↑n))

def const_n (n s : ℕ) : ℝ

Equations

• const_n n s = 1 + sum (↑n) s - sum 1 s + rem_n 1 (n - 1) s

def const (s : ℕ) : ℝ

Equations

• const s = 1 - sum 1 s + rem 1 s

theorem log_rising_em (x : ℝ) (n s : ℕ) (x0 : 0 < x) : log_rising x n = 2⁻¹ * (Real.log x + Real.log (x + ↑n)) + (x + ↑n) * Real.log (x + ↑n) - x * Real.log x - ↑n + sum (x + ↑n) s - sum x s + rem_n x n s

theorem logGammaSeq_em (x : ℝ) (n s : ℕ) (x0 : 0 < x) (n1 : 1 ≤ n) : Real.BohrMollerup.logGammaSeq x n = pre_n x n + const_n n s + (x - 2⁻¹) * Real.log x - sum (x + ↑n) s + sum x s - rem_n x n s

theorem tendsto_pre {x : ℝ} : Filter.Tendsto (pre_n x) Filter.atTop (nhds (-x))

theorem tendsto_sum {x : ℝ} {s : ℕ} (x0 : 0 ≤ x) : Filter.Tendsto (fun (n : ℕ) => sum (x + ↑n) s) Filter.atTop (nhds 0)

theorem integrableOn_bound {c x : ℝ} {s : ℕ} (x0 : 0 < x) : MeasureTheory.IntegrableOn (fun (t : ℝ) => c * (x + t) ^ (-↑s - 2)) (Set.Ioi 0) MeasureTheory.volume

theorem integrableOn_bound' {c x : ℝ} {s : ℕ} (x0 : 0 < x) : MeasureTheory.IntegrableOn (fun (t : ℝ) => c / (x + t) ^ (s + 2)) (Set.Ioi 0) MeasureTheory.volume

theorem tendsto_rem {x : ℝ} {s : ℕ} (x0 : 0 < x) : Filter.Tendsto (fun (n : ℕ) => rem_n x n s) Filter.atTop (nhds (rem x s))

theorem tendsto_const {s : ℕ} : Filter.Tendsto (fun (n : ℕ) => const_n n s) Filter.atTop (nhds (const s))

theorem log_gamma_em (x : ℝ) (s : ℕ) (x0 : 0 < x) : Real.log (Real.Gamma x) = (x - 2⁻¹) * Real.log x - x + const s + sum x s - rem x s

Delegate the constant to Stirling's formula

theorem MeasureTheory.norm_set_integral_le_set_integral_norm {α : Type u_1} {G : Type u_2} [NormedAddCommGroup G] [NormedSpace ℝ G] {m : MeasurableSpace α} {μ : Measure α} (f : α → G) (s : Set α) : ‖∫ (a : α) in s, f a ∂μ‖ ≤ ∫ (a : α) in s, ‖f a‖ ∂μ

theorem MeasureTheory.norm_set_integral_le_of_norm_le {α : Type u_1} {G : Type u_2} [NormedAddCommGroup G] [NormedSpace ℝ G] {m : MeasurableSpace α} {μ : Measure α} {f : α → G} {g : α → ℝ} {s : Set α} (hg : IntegrableOn g s μ) (h : ∀ᵐ (x : α) ∂μ.restrict s, ‖f x‖ ≤ g x) : ‖∫ (x : α) in s, f x ∂μ‖ ≤ ∫ (x : α) in s, g x ∂μ

theorem tendsto_sum_atTop {s : ℕ} : Filter.Tendsto (fun (x : ℝ) => sum x s) Filter.atTop (nhds 0)

theorem integral_bound {c x a : ℝ} (x0 : 0 < x) (a1 : a < -1) : ∫ (t : ℝ) in Set.Ioi 0, c * (x + t) ^ a = c * (x ^ (a + 1) / (-a - 1))

theorem tendsto_rem_atTop {s : ℕ} : Filter.Tendsto (fun (x : ℝ) => rem x s) Filter.atTop (nhds 0)

theorem tendsto_log_gamma_stirling : Filter.Tendsto (fun (n : ℕ) => Real.log (Real.Gamma ↑n) - (↑n - 2⁻¹) * Real.log ↑n + ↑n) Filter.atTop (nhds (Real.log (2 * Real.pi) / 2))

theorem const_eq (s : ℕ) : const s = Real.log (2 * Real.pi) / 2

Sum needs only even powers

theorem Finset.sum_range_even_odd {α : Type u_1} [AddCommMonoid α] {f : ℕ → α} {n : ℕ} : ∑ k ∈ range n, f k = ∑ k ∈ range ((n + 1) / 2), f (2 * k) + ∑ k ∈ range (n / 2), f (2 * k + 1)

theorem sum_eq_even (x : ℝ) (s : ℕ) : sum x (2 * s) = ∑ m ∈ Finset.range (s + 1), term x (2 * m)

Bounding the remainder

theorem abs_rem_le (x : ℝ) (s : ℕ) (e : Even s) (x0 : 0 < x) : |rem x s| ≤ ↑|bernoulli (s + 2)| / (↑s + 1) / (↑s + 2) / x ^ (s + 1)

Not sure if this is tight

theorem abs_rem_le' (x : ℝ) (s : ℕ) (e : Even s) (x0 : 0 < x) : |rem x s| ≤ |term x s|

Not sure if this is tight

The main result, stated succinctly

theorem term_eq (x : ℝ) (s : ℕ) : term x s = ↑(bernoulli (s + 2)) / ((↑s + 1) * (↑s + 2)) / x ^ (s + 1)

Each term in the Stirling series

theorem abs_log_gamma_sub_le (x : ℝ) (x0 : 0 < x) (s : ℕ) : |Real.log (Real.Gamma x) - ((x - 2⁻¹) * Real.log x - x + Real.log (2 * Real.pi) / 2 + ∑ m ∈ Finset.range (s + 1), term x (2 * m))| ≤ |term x (2 * s)|

Effective Stirling series for log Gamma, but with a non-tight remainder bound