Log tables

Stream: PrimeNumberTheorem+

[Li Xuanji]

For fun, I tried to work on kernel-checked proofs of numeric bounds on log 2 and it turned out pretty short. I'd be pretty interested to see this as a "challenge / benchmark problem", in particular to see if there are faster-converging series (the series I'm using converges at 0.95 decimal digits per term, but that seems pretty slow when compared to e.g. fast-converging series for pi). Depending on the terms of the challenge, there might also be a trade-off where a fast-converging series identity is hard to prove.

/-
Copyright (c) 2025. All rights reserved.
Released under MIT license.

Bounds on ln(2) using the atanh series:
  ln(z) = 2 * Σ_{k=0}^∞ (1/(2k+1)) * ((z-1)/(z+1))^(2k+1)

For z = 2, this becomes:
  ln(2) = 2 * Σ_{k=0}^∞ (1/(2k+1)) * (1/3)^(2k+1)

This is the series expansion of 2·atanh((z-1)/(z+1)), using the identity
ln(z) = 2·atanh((z-1)/(z+1)) for z > 0.

Convergence rate: Each term provides approximately log₁₀(9) ≈ 0.95 decimal
digits of precision, since the exponent increases by 2 and (1/3)^2 = 1/9.

Main results:
- `log_2_gt`: 0.693147 < ln(2)  (6 terms, partial sum lower bound)
- `log_2_lt`: ln(2) < 0.693148  (7 terms + geometric tail bound)
-/
import Mathlib

/-! ## Main series representation theorem -/

/-- The series representation of ln(z) for positive z -/
theorem log_eq_hasSum_atanh {z : ℝ} (hz : 0 < z) :
    HasSum (fun k : ℕ => 2 * (1 / (2 * k + 1)) * ((z - 1) / (z + 1)) ^ (2 * k + 1)) (Real.log z) := by
  set x := (z - 1) / (z + 1) with hx_def
  have habs : |x| < 1 := by
    rw [hx_def, abs_div]
    have hz1 : 0 < z + 1 := by linarith
    rw [abs_of_pos hz1]
    have h1 : |z - 1| < z + 1 := by
      by_cases h : 1 ≤ z
      · rw [abs_of_nonneg (by linarith : 0 ≤ z - 1)]; linarith
      · push_neg at h
        rw [abs_of_neg (by linarith : z - 1 < 0)]; linarith
    calc |z - 1| / (z + 1) < (z + 1) / (z + 1) := div_lt_div_of_pos_right h1 hz1
      _ = 1 := div_self (ne_of_gt hz1)
  have hs := Real.hasSum_log_sub_log_of_abs_lt_one habs
  have hz1_ne : z + 1 ≠ 0 := by linarith
  have one_plus_x : 1 + x = 2 * z / (z + 1) := by rw [hx_def]; field_simp; ring
  have one_minus_x : 1 - x = 2 / (z + 1) := by rw [hx_def]; field_simp; ring
  have h2z_pos : 0 < 2 * z := by linarith
  have h2_pos : (0 : ℝ) < 2 := by norm_num
  rw [one_plus_x, one_minus_x] at hs
  rw [Real.log_div (ne_of_gt h2z_pos) hz1_ne] at hs
  rw [Real.log_div (ne_of_gt h2_pos) hz1_ne] at hs
  convert hs using 1
  rw [Real.log_mul (ne_of_gt h2_pos) (ne_of_gt hz)]
  ring

theorem summable_log_atanh {z : ℝ} (hz : 0 < z) :
    Summable (fun k : ℕ => 2 * (1 / (2 * k + 1)) * ((z - 1) / (z + 1)) ^ (2 * k + 1)) :=
  (log_eq_hasSum_atanh hz).summable

/-! ## Specialization to z = 2 -/

/-- The k-th term of the series for ln(2): 2 * (1/(2k+1)) * (1/3)^(2k+1) -/
noncomputable def log_two_term (k : ℕ) : ℝ := 2 * (1 / (2 * k + 1)) * (1/3 : ℝ) ^ (2 * k + 1)

theorem summable_log_two_series : Summable log_two_term := by
  have h := summable_log_atanh (by norm_num : (0:ℝ) < 2)
  convert h using 1
  ext k
  simp only [log_two_term]
  norm_num

theorem log_two_eq_tsum : Real.log 2 = ∑' (k : ℕ), log_two_term k := by
  have h := log_eq_hasSum_atanh (by norm_num : (0:ℝ) < 2)
  have heq : ∀ k, 2 * (1 / (2 * ↑k + 1)) * ((2 - 1) / (2 + 1)) ^ (2 * k + 1) = log_two_term k := by
    intro k; simp only [log_two_term]; norm_num
  simp only [heq] at h
  exact h.tsum_eq.symm

/-! ## Lower bound theorem -/

/-- Lower bound on log 2 from first 6 terms of the series 2Σ (1/(2k+1))(1/3)^(2k+1):
    0.693147 < ln(2)

    The partial sum of 6 terms equals 15757912/22733865 ≈ 0.6931471806,
    which exceeds 0.693147. Since all remaining terms are positive, the full
    series (which equals ln(2)) is strictly greater than the partial sum.
-/
theorem log_2_gt : (0.693147 : ℝ) < Real.log 2 := by
  rw [log_two_eq_tsum]
  -- Partial sum of 6 terms: 15757912/22733865 > 0.693147
  have hpartial : ∑ k ∈ Finset.range 6, log_two_term k = 15757912 / 22733865 := by
    simp only [log_two_term]
    norm_num
  have hbound : (0.693147 : ℝ) < 15757912 / 22733865 := by norm_num
  calc (0.693147 : ℝ)
      < 15757912 / 22733865 := hbound
    _ = ∑ k ∈ Finset.range 6, log_two_term k := hpartial.symm
    _ < ∑' (k : ℕ), log_two_term k := by
        have hdecomp := summable_log_two_series.sum_add_tsum_compl (s := Finset.range 6)
        rw [← hdecomp]
        set S := (↑(Finset.range 6) : Set ℕ)ᶜ with hS_def
        suffices h : 0 < ∑' (x : S), log_two_term x by linarith
        have hmem : (6 : ℕ) ∈ S := by simp [hS_def]
        have hsum := summable_log_two_series.subtype S
        have hnn : ∀ (i : S), 0 ≤ log_two_term i := by
          intro ⟨i, _⟩
          simp only [log_two_term]
          positivity
        exact hsum.tsum_pos hnn ⟨6, hmem⟩ (by simp [log_two_term]; positivity)

/-! ## Upper bound theorem -/

/-- Bound: each term is at most 2 * (1/3)^(2k+1) -/
theorem log_two_term_le (k : ℕ) : log_two_term k ≤ 2 * (1/3 : ℝ) ^ (2 * k + 1) := by
  simp only [log_two_term]
  have h1 : (0 : ℝ) < 2 * k + 1 := by positivity
  have h2 : 1 / (2 * (k : ℝ) + 1) ≤ 1 := by
    rw [div_le_one h1]
    have hk : (0 : ℝ) ≤ k := Nat.cast_nonneg k
    linarith
  have h3 : (0 : ℝ) < (1/3 : ℝ) ^ (2 * k + 1) := by positivity
  have h4 : (0 : ℝ) ≤ (1/3 : ℝ) ^ (2 * k + 1) := le_of_lt h3
  calc 2 * (1 / (2 * k + 1)) * (1/3 : ℝ) ^ (2 * k + 1)
      ≤ 2 * 1 * (1/3 : ℝ) ^ (2 * k + 1) := by nlinarith
    _ = 2 * (1/3 : ℝ) ^ (2 * k + 1) := by ring

theorem summable_geo_bound : Summable (fun k : ℕ => (2 : ℝ) * (1/3) ^ (2 * k + 1)) := by
  have h : Summable (fun k : ℕ => (2/3 : ℝ) * (1/9) ^ k) := by
    apply Summable.mul_left
    exact summable_geometric_of_lt_one (by norm_num) (by norm_num)
  convert h using 1
  ext k
  have : (1/3 : ℝ) ^ (2 * k + 1) = (1/3) * (1/9)^k := by
    rw [pow_add, pow_mul]
    norm_num
    ring
  linarith

/-- Tail bound: Σ_{k≥K} log_two_term k ≤ (9/4) * (1/3)^(2K+1) -/
theorem tail_bound (K : ℕ) : ∑' k, log_two_term (K + k) ≤ (9/4 : ℝ) * (1/3) ^ (2 * K + 1) := by
  have hsummable : Summable (fun k => log_two_term (K + k)) :=
    summable_log_two_series.comp_injective (fun _ _ h => Nat.add_left_cancel h)
  have hsummable_geo : Summable (fun k => (2 : ℝ) * (1/3) ^ (2 * (K + k) + 1)) :=
    summable_geo_bound.comp_injective (fun _ _ h => Nat.add_left_cancel h)
  have hle : ∀ k, log_two_term (K + k) ≤ 2 * (1/3 : ℝ) ^ (2 * (K + k) + 1) := fun k => log_two_term_le (K + k)
  have hsum_le : ∑' k, log_two_term (K + k) ≤ ∑' k, (2 : ℝ) * (1/3) ^ (2 * (K + k) + 1) :=
    hsummable.tsum_le_tsum hle hsummable_geo
  have hgeo_eq : ∑' k, (2 : ℝ) * (1/3) ^ (2 * (K + k) + 1) = (9/4) * (1/3) ^ (2 * K + 1) := by
    have factor : ∀ k, (2 : ℝ) * (1/3) ^ (2 * (K + k) + 1) = 2 * (1/3)^(2*K+1) * (1/9)^k := by
      intro k
      have : 2 * (K + k) + 1 = 2 * K + 1 + 2 * k := by ring
      rw [this, pow_add]
      have : (1/3 : ℝ) ^ (2 * k) = (1/9)^k := by rw [pow_mul]; norm_num
      rw [this]
      ring
    simp_rw [factor]
    rw [tsum_mul_left]
    have hgeo : ∑' k : ℕ, (1/9 : ℝ)^k = 9/8 := by
      rw [tsum_geometric_of_lt_one (by norm_num) (by norm_num)]
      norm_num
    rw [hgeo]
    ring
  linarith

/-- Upper bound on log 2 using 7 terms plus geometric tail bound:
    ln(2) < 0.693148

    The partial sum of 7 terms equals 5531027882/7979586615.
    The tail Σ_{k≥7} is bounded by (9/4)·(1/3)^15 = 3/19131876.
    Their sum is less than 0.693148.
-/
theorem log_2_lt : Real.log 2 < (0.693148 : ℝ) := by
  rw [log_two_eq_tsum]
  have hdecomp := Summable.sum_add_tsum_nat_add 7 summable_log_two_series
  rw [← hdecomp]
  have hpartial : ∑ k ∈ Finset.range 7, log_two_term k = 5531027882 / 7979586615 := by
    simp only [log_two_term]
    norm_num
  rw [hpartial]
  have htail := tail_bound 7
  have htail_val : (9/4 : ℝ) * (1/3) ^ (2 * 7 + 1) = 3 / 19131876 := by norm_num
  rw [htail_val] at htail
  have htail' : ∑' i, log_two_term (i + 7) ≤ 3 / 19131876 := by
    have heq : (fun i => log_two_term (i + 7)) = (fun k => log_two_term (7 + k)) := by
      ext k; ring_nf
    rw [heq]
    exact htail
  have hbound : 5531027882 / 7979586615 + 3 / 19131876 < (0.693148 : ℝ) := by norm_num
  have htail_nn : 0 ≤ ∑' i, log_two_term (i + 7) := by
    apply tsum_nonneg
    intro k
    simp only [log_two_term]
    positivity
  linarith

I'd also be interested in using a series-based approach for bounds on li(2) although I already forsee that the candidate series identity is harder to prove

[Chris Birkbeck]

@Bhavik Mehta has some pretty cool approximations to log that may be useful here.

[Terence Tao]

I would imagine that the power series for exp would converge faster than the known series expansions for log, so one way to show something like (0.693147 : ℝ) < Real.log 2 is to instead show exp (0.693147 : ℝ) < 2. Though maybe at this level of precision this only offers a modest speedup.

[Joseph Myers]

We also have bounds on log 2 in mathlib: docs#Real.log_two_gt_d9 docs#Real.log_two_lt_d9

[Li Xuanji]

Oh nice! Looks like they go through approximations of exp

[Aaron Liu]

I made a thing

the thing is very long

import Mathlib

def LogApprox (q e ε : ℚ) : Prop :=
  0 < q ∧ dist (Real.log q) e ≤ ε

theorem LogApprox.one : LogApprox 1 0 0 := ⟨by norm_num, by simp⟩

theorem LogApprox.init (x e ε : ℚ) (n : ℕ) (hn : n ≠ 0) (hx0 : 0 < x) (h1 : x ≠ 1)
    (he : e = 2 * ∑ i ∈ Finset.range n, ((x - 1) / (x + 1)) ^ (2 * i + 1) / Nat.cast (2 * i + 1))
    (hε : |e| ≤ ε * (((x + 1) / (x - 1)) ^ (2 * n) - 1)) :
    LogApprox x e ε := by
  have hd (u : ℝ) (hul : 1 + u ≠ 0) (hur : 1 - u ≠ 0) :
      HasDerivAt (fun c => Real.log ((1 + c) / (1 - c))) (2 / (1 - u ^ 2)) u := by
    refine .congr_deriv (.log (.div
      ((hasDerivAt_id u).const_add 1)
      ((hasDerivAt_id u).const_sub 1) hur) (div_ne_zero hul hur)) ?_
    have : 1 - u ^ 2 ≠ 0 := Eq.trans_ne (by ring) (mul_ne_zero hul hur)
    field
  let u : ℝ := (x - 1) / (x + 1)
  have hku : (1 + u) / (1 - u) = x := by field
  have hp : u ∈ Set.Ioo (-1) 1 := by
    have hp : 0 < (1 + u) / (1 - u) := lt_of_lt_of_eq (mod_cast hx0) hku.symm
    rw [div_pos_iff, sub_pos, ← neg_lt_iff_pos_add',
      sub_neg, ← lt_neg_iff_add_neg'] at hp
    obtain ⟨hpl, hpr⟩ | ⟨_, _⟩ := hp
    · exact ⟨hpl, hpr⟩
    · linarith
  have hicc (c : ℝ) (hc : c ∈ Set.uIcc 0 u) : c ∈ Set.Ioo (-1) 1 := by
    rw [Set.mem_uIcc] at hc
    obtain ⟨h0c, hcu⟩ | ⟨huc, hc0⟩ := hc
    · exact ⟨lt_of_lt_of_le (by norm_num) h0c, hcu.trans_lt hp.2⟩
    · exact ⟨hp.1.trans_le huc, hc0.trans_lt (by norm_num)⟩
  have hicl (c : ℝ) (hc : c ∈ Set.uIcc 0 u) : 1 + c ≠ 0 := by
    rw [ne_eq, add_eq_zero_iff_neg_eq]
    exact (hicc c hc).1.ne
  have hicr (c : ℝ) (hc : c ∈ Set.uIcc 0 u) : 1 - c ≠ 0 := by
    rw [sub_ne_zero]
    exact (hicc c hc).2.ne'
  have hcc : ContinuousOn (fun c => 2 / (1 - c ^ 2)) (Set.uIcc 0 u) :=
    continuousOn_const.div₀ (continuousOn_const.sub (continuousOn_pow 2))
      fun c hc => Eq.trans_ne (by ring) (mul_ne_zero (hicl c hc) (hicr c hc))
  have hin := intervalIntegral.integral_eq_sub_of_hasDerivAt
    (fun c hc => hd c (hicl c hc) (hicr c hc)) hcc.intervalIntegrable
  rw [add_zero, sub_zero, div_one, Real.log_one, sub_zero, hku] at hin
  have h : dist (Real.log x) e ≤ u ^ (2 * n) * |Real.log x| := by
    rw [Real.dist_eq, ← hin]
    have her : e = 2 * ∑ i ∈ Finset.range n, ∫ y in 0..u, y ^ (2 * i) := by
      rw [he]
      push_cast
      simp [u]
    have ueq : Set.EqOn (fun c => 2 / (1 - c ^ 2) - 2 * ∑ i ∈ Finset.range n, c ^ (2 * i))
        (fun c => (c ^ (2 * n)) * (2 / (1 - c ^ 2))) (Set.uIcc 0 u) := by
      intro c hc
      simp only [pow_mul]
      have hd : 1 - c ^ 2 ≠ 0 := Eq.trans_ne (by ring) (mul_ne_zero (hicl c hc) (hicr c hc))
      rw [geom_sum_eq (sub_ne_zero.1 hd).symm, ← neg_div_neg_eq _ (c ^ 2 - 1), neg_sub (c ^ 2)]
      field
    rw [her, ← intervalIntegral.integral_finset_sum fun i _ =>
      (continuousOn_pow (2 * i)).intervalIntegrable,
      ← intervalIntegral.integral_const_mul,
      ← intervalIntegral.integral_sub hcc.intervalIntegrable
      (continuousOn_const.fun_mul (continuousOn_finset_sum _ fun i hi =>
        continuousOn_pow (2 * i))).intervalIntegrable,
      intervalIntegral.integral_congr ueq,
      intervalIntegral.abs_intervalIntegral_eq, intervalIntegral.abs_intervalIntegral_eq]
    apply MeasureTheory.abs_integral_le_integral_abs.trans
    have hnn (c : ℝ) (hc : c ∈ Set.uIoc 0 u) : 0 ≤ 2 / (1 - c ^ 2) := by
      apply div_nonneg (by norm_num)
      simpa [abs_le] using Set.Ioo_subset_Icc_self (hicc c (Set.uIoc_subset_uIcc hc))
    rw [abs_of_nonneg (MeasureTheory.setIntegral_nonneg measurableSet_uIoc hnn),
      ← MeasureTheory.integral_const_mul]
    apply MeasureTheory.setIntegral_mono_on
      ((ContinuousOn.integrableOn_uIcc (by fun_prop)).mono_set Set.uIoc_subset_uIcc)
      ((ContinuousOn.integrableOn_uIcc (by fun_prop)).mono_set Set.uIoc_subset_uIcc)
      measurableSet_uIoc
    intro c hc
    rw [abs_mul, pow_mul', abs_sq, ← pow_mul', abs_of_nonneg (hnn c hc)]
    apply mul_le_mul_of_nonneg_right
    · rw [pow_mul, pow_mul]
      apply pow_le_pow_left₀ (sq_nonneg c)
      rw [Set.mem_uIoc] at hc
      obtain ⟨hc0, hcu⟩ | ⟨huc, hc0⟩ := hc
      · exact pow_le_pow_left₀ hc0.le hcu 2
      · rw [← neg_sq c, ← neg_sq u]
        exact pow_le_pow_left₀ (neg_nonneg.2 hc0) (neg_le_neg huc.le) 2
    · exact hnn c hc
  refine ⟨hx0, h.trans ?_⟩
  have hup : 0 ≤ u ^ (2 * n) := pow_mul' u 2 n ▸ sq_nonneg (u ^ n)
  have hu1 : 0 < 1 - u ^ (2 * n) := by
    rw [pow_mul, sub_pos]
    exact pow_lt_one₀ (sq_nonneg u) (by simpa [abs_lt] using hp) hn
  calc u ^ (2 * n) * |Real.log x|
    _ = u ^ (2 * n) * |Real.log x| / (1 - u ^ (2 * n)) -
        ((u ^ (2 * n)) ^ 2 * |Real.log x| / (1 - u ^ (2 * n))) := by field
    _ = u ^ (2 * n) * |e - (e - Real.log x)| / (1 - u ^ (2 * n)) -
        ((u ^ (2 * n)) ^ 2 * |Real.log x| / (1 - u ^ (2 * n))) := by simp
    _ ≤ u ^ (2 * n) * (|Rat.cast e| + |e - Real.log x|) / (1 - u ^ (2 * n)) -
        ((u ^ (2 * n)) ^ 2 * |Real.log x| / (1 - u ^ (2 * n))) := by gcongr; apply abs_sub
    _ = u ^ (2 * n) * (|Rat.cast e| + dist (Real.log x) e) / (1 - u ^ (2 * n)) -
        ((u ^ (2 * n)) ^ 2 * |Real.log x| / (1 - u ^ (2 * n))) := by rw [dist_comm, Real.dist_eq]
    _ ≤ u ^ (2 * n) * (|Rat.cast e| + u ^ (2 * n) * |Real.log x|) / (1 - u ^ (2 * n)) -
        ((u ^ (2 * n)) ^ 2 * |Real.log x| / (1 - u ^ (2 * n))) := by gcongr
    _ = |Rat.cast e| * u ^ (2 * n) / (1 - u ^ (2 * n)) := by field
  unfold u
  norm_cast
  have hui : 0 < (x + 1) ^ (2 * n) - (x - 1) ^ (2 * n) := by
    rw [sub_pos, pow_mul, pow_mul]
    exact pow_lt_pow_left₀ (by linarith) (sq_nonneg (x - 1)) hn
  have hou : 0 < (x - 1) ^ (2 * n) := by
    rw [pow_mul', sq_pos_iff]
    exact pow_ne_zero n (sub_ne_zero.2 h1)
  rw [div_pow] at hε ⊢
  field_simp at hε ⊢
  exact hε

theorem LogApprox.step (x e ε x₂ e₂ ε₂ : ℚ) (n : ℤ)
    (h : LogApprox x e ε) (h₂ : LogApprox x₂ e₂ ε₂) :
    LogApprox (x * x₂ ^ n) (e + n * e₂) (ε + |n| * ε₂) := by
  refine ⟨mul_pos h.1 (zpow_pos h₂.1 n), ?_⟩
  push_cast
  rw [Real.log_mul (mod_cast h.1.ne')
    (zpow_ne_zero n (mod_cast h₂.1.ne')),
    Real.log_zpow, Real.dist_eq, add_sub_add_comm]
  apply (abs_add_le _ _).trans
  rw [← mul_sub, abs_mul, ← Real.dist_eq, ← Real.dist_eq]
  exact add_le_add h.2 (mul_le_mul_of_nonneg_left h₂.2 (abs_nonneg (Int.cast n)))

theorem LogApprox.mono (x e ε x₂ e₂ ε₂ : ℚ) (h : LogApprox x e ε)
    (hx : x₂ = x) (h₂ : |e₂ - e| ≤ ε₂ - ε) : LogApprox x₂ e₂ ε₂ := by
  cases hx
  refine ⟨h.1, ?_⟩
  have ho := h.2
  rw [Real.dist_eq, abs_le] at ho ⊢
  rw [abs_le] at h₂
  rify at h₂
  cases ho; cases h₂; constructor <;> linarith

open Lean Meta Elab Tactic Qq

def proveLogApprox (l : List (Rat × Int × Nat)) :
    Except String ((q : Rat) × (e : Rat) × (ε : Rat) × Q(LogApprox $q $e $ε)) := do
  match l with
  | [] => return ⟨1, 0, 0, q(.one)⟩
  | (x, n, p) :: xs =>
    if x ≤ 0 then throw s!"{x} is not strictly positive"
    let k : ℕ := p + 1
    let c : ℚ := 2 * ∑ i ∈ Finset.range k, ((x - 1) / (x + 1)) ^ (2 * i + 1) / Nat.cast (2 * i + 1)
    let ε : ℚ := |c| / (((x + 1) / (x - 1)) ^ (2 * k) - 1)
    let ⟨x₁, e₁, ε₁, h₁⟩ ← proveLogApprox xs
    if x = 1 then return ⟨x₁, e₁, ε₁, h₁⟩
    have ne : Q(decide ($x ≠ 1) = true) := reflBoolTrue
    have pos : Q(decide (0 < $x) = true) := reflBoolTrue
    have ineq : Q(decide (|$c| ≤ $ε * ((($x + 1) / ($x - 1)) ^ (2 * $k) - 1)) = true) :=
      reflBoolTrue
    let prf1 : Q(LogApprox $x $c $ε) :=
      q(.init $x $c $ε $k (Nat.add_one_ne_zero $p)
        (of_decide_eq_true $pos) (of_decide_eq_true $ne)
        (Eq.refl $c) (of_decide_eq_true $ineq))
    return ⟨x₁ * x ^ n, e₁ + n * c, ε₁ + |n| * ε,
      q(LogApprox.step $x₁ $e₁ $ε₁ $x $c $ε $n $h₁ $prf1)⟩

syntax logApproxTerm := num " / " num (" ^ " num)? (", " num)?

def parseLogApproxTerm (s : TSyntax ``logApproxTerm) : CoreM (Rat × Int × Nat) :=
  match s with
  | `(logApproxTerm| $u:num / $v:num $[^ $n:num]? $[, $p:num]?) =>
    let u := u.getNat
    let v := v.getNat
    let n := n.elim 1 (·.getNat)
    let p := p.elim 2 (·.getNat)
    return (u / v, n, p)
  | _ => throwUnsupportedSyntax

elab (name := logApprox) "log_approx" "[" ts:sepBy1(logApproxTerm, ";") "]" : tactic => do
  let goal ← getMainGoal
  goal.withContext do
    let goalType ← goal.getType
    let some tt ← checkTypeQ goalType q(Prop) |
      throwError "target{indentExpr goalType} is not a proposition"
    let l ← liftM <| ts.getElems.mapM parseLogApproxTerm
    match tt with
    | ~q(LogApprox $q $e $ε) =>
      match proveLogApprox l.toList with
      | .ok ⟨q', e', ε', pf⟩ =>
        let eq ← mkFreshExprMVarQ q($q = $q') .syntheticOpaque `eq
        let le ← mkFreshExprMVarQ q(|$e - $e'| ≤ $ε - $ε') .syntheticOpaque `le
        let prf : Q(LogApprox $q $e $ε) := q(.mono $q' $e' $ε' $q $e $ε $pf $eq $le)
        goal.assign prf
        pushGoals [eq.mvarId!, le.mvarId!]
      | .error str => throwError str
    | _ => throwError "target{indentExpr tt} is not of the form `LogApprox ?q ?e ?ε`"

example : LogApprox 2 0.693148 0.000001 := by
  log_approx [10 / 9 ^ 7; 24 / 25 ^ 2; 81 / 80 ^ 3] <;> norm_num
example : LogApprox 3 1.098612 0.000001 := by
  log_approx [10 / 9 ^ 11; 24 / 25 ^ 3; 81 / 80 ^ 5] <;> norm_num

[Aaron Liu]

you can use it to prove log approximations

[Bhavik Mehta]

I'm not at home, but in another thread I posted code which gave log 2 up to a million digits, and I also have code which gives arbitrary logs to 30 (though it's adjustable) precision

[Aaron Liu]

nice

[Aaron Liu]

found it: #general > A million digits of log 2 @ 💬

[Bhavik Mehta]

The formula I used was the last one from this list: https://en.wikipedia.org/wiki/Natural_logarithm_of_2#Series_representations

[Aaron Liu]

oh I didn't realize we had these bounds on artanh already in mathlib

[Aaron Liu]

I was searching for @loogle Real.artanh

[loogle]

:search: Real.artanh, Real.artanh_tanh, and 20 more

[Aaron Liu]

and didn't end up finding anything useful so I proved some myself

[Bhavik Mehta]

I added them before we had artanh itself, certainly it should be stated using that def now