Lower bound for log(x + 1)

Stream: Is there code for X?

[Jakob von Raumer]

I needed this lower bound for $\log (x + 1)$ for something else, the proof is basically copied from this stackexchange post, is that too specific for Mathlib? Afaik there's no other rational lower bound so far.

lemma Real.lt_log_add_one_of_pos {x : ℝ} (hx : 0 < x) : 2 * x / (x + 2) < log (x + 1) :=
  have : ∀ {t}, 0 < t → (4 : ℝ) / (t + 2) ^ 2 < 1 / (t + 1) := fun ht => by
    apply lt_of_sub_pos
    rw [div_sub_div _ _ (by positivity) (by positivity)]
    conv_rhs => enter [1]; ring_nf
    positivity
  have : ∫ (t : ℝ) in (0)..x, 4 / (t + 2) ^ 2 < ∫ (t : ℝ) in (0)..x, 1 / (t + 1) :=
    intervalIntegral.integral_lt_integral_of_continuousOn_of_le_of_exists_lt hx
      (continuousOn_const.div₀ ((continuousOn_id.add continuousOn_const).pow 2)
        fun _ ⟨_, _⟩ => (by positivity))
      (continuousOn_const.div₀ (continuousOn_id.add continuousOn_const)
        fun _ ht => by rcases ht; positivity)
      (fun _ ht => le_of_lt (this ht.1)) ⟨x, by simp_all [le_of_lt hx], this hx⟩
  calc 2 * x / (x + 2) = ∫ t in (0).. x, 4 / (t + 2) ^ (2 : ℕ) := by {
      rw [intervalIntegral.integral_comp_add_right (fun t => 4 / t ^ (2 : ℕ))]
      simp only [← mul_one_div (4 : ℝ), one_div]
      rw [intervalIntegral.integral_const_mul,
        intervalIntegral.integral_congr_ae (g := (· ^ (- (2 : ℝ)))) <|
        MeasureTheory.ae_of_all _ fun t ⟨ht, ht'⟩ => by
          simp only [zero_add, inf_lt_iff, le_sup_iff, rpow_two] at ht ht' ⊢
          rw [← rpow_two, rpow_neg]
          rcases ht with ht|ht <;> rcases ht' with ht'|ht' <;> linarith,
        integral_rpow
          (.inr ⟨by norm_num, Set.not_mem_Icc_of_lt (lt_min (by norm_num) (by positivity))⟩)]
      norm_num
      rw [div_neg, div_one, neg_sub, rpow_neg_one, mul_sub, div_eq_of_eq_mul (by positivity)]
      rw [sub_mul, inv_mul_cancel_right₀]
      ring_nf
      apply ne_of_gt (by positivity) }
    _ < ∫ t in (0)..x, 1 / (t + 1) := this
    _ = log (x + 1) := by
      rw [intervalIntegral.integral_comp_add_right,
        integral_one_div (Set.not_mem_Icc_of_lt (lt_min (by norm_num) (by positivity)))]
      simp

[Kevin Buzzard]

This is correct to O(x^3) so I would imagine that it would be useful esp for small x!

[Jakob von Raumer]

Where do you think it should live, esp since the proof depends on intervalIntegral?

[Kevin Buzzard]

What does #find_home say?

[Jakob von Raumer]

Tells me the name of the File that contains only the lemma itself :disappointed:

[Ben Eltschig]

Mathlib.Analysis.SpecialFunctions.Integrals is what it told me in the browser

[Jakob von Raumer]

Might be a bit weird because the final statement doesn't contain the integrals anymore, but I can't think of anything else that wouldn't cause big changes to the import graph

[Jz Pan]

Are there any other proofs not involving integral? For example, can you prove 2 * x < (x + 2) * log (x + 1) instead, by taking derivatives?

[Jz Pan]

I think this works: let $f(x)=(x+2)\log(x+1)-2x$, then $f'(x)=\frac{1}{x+1}+\log(x+1)-1$, $f''(x)=\frac{1}{x+1}-\frac{1}{(x+1)^2}$, it's clear that $f(0)=f'(0)=f''(0)=0$ while $f''(x)>0$ for $x>0$, hence $f(x)>0$ for $x>0$.

[Jireh Loreaux]

It would be nice to get the BigO result Kevin mentioned too while you're at it.

[Jakob von Raumer]

@Jz Pan I'll see if that's shorter! I actually stopped looking for alternative proofs once if found the thing on stackexchange :sweat_smile:

[Jakob von Raumer]

@Jireh Loreaux Will have a look at it

[Thomas Browning]

Here's a short proof of the weak inequality. The strict inequality would require a lemma lt_hasSum.

lemma Real.lt_log_add_one_of_pos {x : ℝ} (hx : 0 < x) : 2 * x / (x + 2) ≤ log (x + 1) := by
  have key := le_hasSum (Real.hasSum_log_one_add_inv (inv_pos.mpr hx)) 0 (by intros; positivity)
  field_simp [add_comm x] at *
  exact key

[Jz Pan]

Is #21671 your PR?

[Jakob von Raumer]

Yes, happy for you or @Thomas Browning to just push on the branch and replace the overcomplicated proof there!

[Jz Pan]

I'm not familiar with analytic part of mathlib, so I don't know how to formalize it...

[Jakob von Raumer]

I guess @Thomas Browning's proof is as short as it can get, but I'd also be interested in seeing your approach being formalized. There's probably a bunch of lemmas that provide monotonicity of $f$ in the case of $f'(x) > 0$

[Jireh Loreaux]

docs#strictMono_of_deriv_pos

[Jz Pan]

Jakob von Raumer said:

I guess Thomas Browning's proof is as short as it can get

The complexity is hiding into docs#Real.hasSum_log_one_add_inv :joy:

[Jz Pan]

I have finished the elementary proof which only uses derivatives. But it's quite long...

import Mathlib.Analysis.SpecialFunctions.Integrals

lemma Real.lt_log_add_one_of_pos {x : ℝ} (hx : 0 < x) : 2 * x / (x + 2) < log (x + 1) := by
  rw [div_lt_iff₀ (by positivity), ← sub_pos, mul_comm 2 x]
  let f (x : ℝ) := log (x + 1) * (x + 2) - x * 2
  let f' (x : ℝ) := (x + 1)⁻¹ + log (x + 1) - 1
  let f'' (x : ℝ) := -1 / (x + 1) ^ 2 + (x + 1)⁻¹
  have hda1 (x : ℝ) (hx : 0 ≤ x) : DifferentiableAt ℝ (fun x ↦ log (x + 1)) x :=
    .comp (f := (· + 1)) x (g := log)
      (Real.differentiableAt_log (by positivity)) (by simp)
  have hd1 (x : ℝ) (hx : 0 ≤ x) : deriv (fun x ↦ log (x + 1)) x = (x + 1)⁻¹ := by
    simpa using deriv_comp x (h := (· + 1)) (h₂ := log)
      (Real.differentiableAt_log (by positivity)) (by simp)
  have hf (x : ℝ) (hx : 0 ≤ x) : deriv f x = f' x := by
    simp_rw [f, f']
    trans (x + 1)⁻¹ * (x + 2) + log (x + 1) - 2
    · simp [hda1 x hx, hd1 x hx]
    nth_rw 1 [← one_add_one_eq_two]
    rw [← add_assoc, mul_add, inv_mul_cancel₀ (by positivity), mul_one]
    ring1
  have hf' (x : ℝ) (hx : 0 ≤ x) : deriv f' x = f'' x := by
    have hx1 : x + 1 ≠ 0 := by positivity
    simp [f', f'', hx1, hda1 x hx, hd1 x hx]
  have hf'm : StrictMonoOn f' (Set.Ici 0) := by
    apply strictMonoOn_of_deriv_pos (convex_Ici 0)
    · intro x hx
      rw [Set.mem_Ici] at hx
      apply ContinuousAt.continuousWithinAt
      apply DifferentiableAt.continuousAt (𝕜 := ℝ)
      simp [f', show x + 1 ≠ 0 by positivity]
    · intro x hx
      simp only [Set.nonempty_Iio, interior_Ici', Set.mem_Ioi] at hx
      simp_rw [hf' x hx.le, f'', neg_div, lt_neg_add_iff_add_lt, add_zero]
      rw [div_lt_iff₀ (by positivity), pow_two, ← mul_assoc, inv_mul_cancel₀ (by positivity)]
      linarith only [hx]
  have hfm : StrictMonoOn f (Set.Ici 0) := by
    apply strictMonoOn_of_deriv_pos (convex_Ici 0)
    · intro x hx
      rw [Set.mem_Ici] at hx
      apply ContinuousAt.continuousWithinAt
      apply DifferentiableAt.continuousAt (𝕜 := ℝ)
      simp [f, show x + 1 ≠ 0 by positivity]
    · intro x hx
      simp only [Set.nonempty_Iio, interior_Ici', Set.mem_Ioi] at hx
      simpa [hf x hx.le, f'] using hf'm (a := 0) (by simp) hx.le hx
  simpa [f] using hfm (a := 0) (by simp) hx.le hx

[Jz Pan]

It turns out that DifferentiableAt has more simp lemmas than ContinuousAt :sweat_smile: This is why I use the former to prove the latter.

[Jakob von Raumer]

Cool, thanks! :tada:

[Bhavik Mehta]

Jakob von Raumer said:

Afaik there's no other rational lower bound so far.

docs#Real.one_sub_inv_le_log_of_pos is a rational lower bound, but it's a priori weaker than yours.

[Jakob von Raumer]

@Jireh Loreaux @Kevin Buzzard This is the result you're referring to, right? (First time I've used the asymptotics)

(fun (x : ℝ) => 2 * x / (x + 2)) =O[𝓝 0] fun x => Real.log (1 + x)

[Jakob von Raumer]

Ah no, this doesn't mention the exponent of the approximation

[Jakob von Raumer]

This?

theorem foo : (fun (x : ℝ) => .log (1 + x) - 2 * x / (x + 2)) =o[𝓝 0] fun x => x ^ 3 := sorry

[Kevin Buzzard]

I would guess it's big O not little o, but apart from that I think so

[Jakob von Raumer]

But even $\frac{\log (1 + x) - \frac{2 x}{x + 2}}{x ^ 2}$ is bounded near zero, shouldn't it be $\mathcal{O}(x^2)$ then?

[Jz Pan]

$\log (1 + x) - \frac{2 x}{x + 2}=\frac{1}{12}x^3+O(x^4)$.

[Jakob von Raumer]

So we'd have this?

theorem foo : (fun (x : ℝ) => .log (1 + x) - (2 * x / (x + 2) + 1 / 12 * x^ 3) =O[𝓝 0] fun x => x ^ 4 := sorry

[Bhavik Mehta]

Can't you get something stronger from the existing taylor series for log? I used this at one point to get very tight rational estimates on log((1+x)/(1-x)), I expect it'll work here too

[Jakob von Raumer]

Where to stop? Don't I get a stronger approximation for every partial sum?

[Bhavik Mehta]

Absolutely, you can just stop when the approximation is good enough for your purpose. The original post here was just one potential place you could stop

[Jz Pan]

Jakob von Raumer said:

So we'd have this?

theorem foo : (fun (x : ℝ) => .log (1 + x) - (2 * x / (x + 2) + 1 / 12 * x^ 3) =O[𝓝 0] fun x => x ^ 4 := sorry

No, I just mean that in particular it is $O(x^3)$ but not $o(x^3)$.