The truncated logarithmic kernel L_{a,b} and its limit log r

• Ltr_eq_v : L_{a,b}(r) = (1/2) ∫_1^{r²} (e^{-av} - e^{-bv})/v dv for r > 0;
• abs_Ltr_le : |L_{a,b}(r)| ≤ |log r|;
• continuous_Ltr : continuity in r;
• tendsto_Ltr : L_{1/(n+1), n+1}(r) → log r.

theorem Zeta5Irrational.integral_exp_neg_mul' {k : ℝ} (hk : k ≠ 0) (c d : ℝ) : ∫ (x : ℝ) in c..d, Real.exp (-k * x) = (Real.exp (-k * c) - Real.exp (-k * d)) / k

theorem Zeta5Irrational.intervalIntegral_swap_of_continuous' {f : ℝ → ℝ → ℝ} (hf : Continuous (Function.uncurry f)) (a b c d : ℝ) : ∫ (x : ℝ) in a..b, ∫ (y : ℝ) in c..d, f x y = ∫ (y : ℝ) in c..d, ∫ (x : ℝ) in a..b, f x y

Fubini for interval integrals of continuous functions, arbitrary orientation.

theorem Zeta5Irrational.Ltr_eq_v {a b r : ℝ} (ha : 0 < a) (hab : a ≤ b) (hr : 0 < r) : Ltr a b r = 1 / 2 * ∫ (v : ℝ) in 1..r ^ 2, (Real.exp (-a * v) - Real.exp (-b * v)) / v

The substituted form of the truncated kernel.

theorem Zeta5Irrational.Ltr_integrand_bounds {a b v : ℝ} (ha : 0 < a) (hab : a ≤ b) (hv : 0 < v) : 0 ≤ (Real.exp (-a * v) - Real.exp (-b * v)) / v ∧ (Real.exp (-a * v) - Real.exp (-b * v)) / v ≤ 1 / v

theorem Zeta5Irrational.continuous_Ltr_integrand {a b : ℝ} (_ha : 0 < a) : Continuous fun (v : ℝ) => (Real.exp (-a * v) - Real.exp (-b * v)) * (max v 1)⁻¹

theorem Zeta5Irrational.intervalIntegrable_of_pos {F : ℝ → ℝ} (hF : Continuous F) {c d : ℝ} (hc : 0 < c) (hd : 0 < d) : IntervalIntegrable (fun (v : ℝ) => F v / v) MeasureTheory.volume c d

theorem Zeta5Irrational.log_eq_half_integral {r : ℝ} (hr : 0 < r) : Real.log r = 1 / 2 * ∫ (v : ℝ) in 1..r ^ 2, 1 / v

theorem Zeta5Irrational.abs_Ltr_le {a b r : ℝ} (ha : 0 < a) (hab : a ≤ b) (hr : 0 < r) : |Ltr a b r| ≤ |Real.log r|

|L_{a,b}(r)| ≤ |log r| for r > 0.

theorem Zeta5Irrational.continuous_Ltr {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) : Continuous fun (r : ℝ) => Ltr a b r

Continuity of the truncated kernel in r.

theorem Zeta5Irrational.log_sub_Ltr {a b r : ℝ} (ha : 0 < a) (hab : a ≤ b) (hr : 0 < r) : Real.log r - Ltr a b r = 1 / 2 * ∫ (v : ℝ) in 1..r ^ 2, (1 - Real.exp (-a * v) + Real.exp (-b * v)) / v

The difference log r - L_{a,b}(r) as an integral.

theorem Zeta5Irrational.diff_integrand_bounds {a b m v : ℝ} (ha : 0 < a) (hab : a ≤ b) (hm : 0 < m) (hv : m ≤ v) : 0 ≤ (1 - Real.exp (-a * v) + Real.exp (-b * v)) / v ∧ (1 - Real.exp (-a * v) + Real.exp (-b * v)) / v ≤ a + Real.exp (-b * m) / m

theorem Zeta5Irrational.abs_log_sub_Ltr_le {a b r : ℝ} (ha : 0 < a) (hab : a ≤ b) (hr : 0 < r) : |Real.log r - Ltr a b r| ≤ 1 / 2 * ((a + Real.exp (-b * min 1 (r ^ 2)) / min 1 (r ^ 2)) * |r ^ 2 - 1|)

|log r - L_{a,b}(r)| ≤ (1/2) |r² - 1| (a + e^{-b m}/m) with m = min 1 r².

theorem Zeta5Irrational.tendsto_Ltr {r : ℝ} (hr : 0 < r) : Filter.Tendsto (fun (n : ℕ) => Ltr (1 / (↑n + 1)) (↑n + 1) r) Filter.atTop (nhds (Real.log r))

Convergence of the truncated kernel to the logarithm.