Integrability of log in a closed interval containing zero

Stream: Is there code for X?

[Stefan Kebekus]

Dear all,

I am stuck trying to compute very elementary integrals such as $\int_0^1 \ln x dx$, and I cannot figure out what theorems of Mathlib would apply in this setting. Any help is greatly appreciated!

Best,

Stefan.

PS: I really want slightly more elaborate integrals of elementary complex analysis, such as $\int_0^{2π} \ln (4*\sin^2 (θ/2)) dθ$, but maybe I should start with the first case I cannot handle…

[Johan Commelin]

Hmm, there is docs#integral_log, but it seems that mathlib really doesn't like having 0 in the domain of integration of log.

[Gareth Ma]

Without looking into the actual Mathlib implementation of the details, you can always prove the Tendsto result instead, i.e. $\lim_{\varepsilon \to 0} \int_{\varepsilon}^1 \log(x) \mathrm{d}x$

[Gareth Ma]

@\Stefan, indeed it would be nice to have $\int_0^{\pi / 2} \log(\sin x) \mathrm{d}x$ in Mathlib (or other upper bounds), and $\int_0^{\pi / 4} \log(\tan x) \mathrm{d}x$ would be fun* to formalise too, IIRC it's not in Mathlib.

*My definition of fun is usually different from others. In this case it's from when I learned it for an integration competition(?) I wonder how hard would it be to formalise the typical proof, which is quite handwavy with series expansion everywhere..

[Johan Commelin]

Gareth Ma said:

Without looking into the actual Mathlib implementation of the details, you can always prove the Tendsto result instead, i.e. $\lim_{\varepsilon \to 0} \int_{\varepsilon}^1 \log(x) \mathrm{d}x$

Do we have the API to make this easy? I can't find it.

cc @Yury G. Kudryashov @Floris van Doorn @Sébastien Gouëzel

[Gareth Ma]

import Mathlib.Analysis.SpecialFunctions.Integrals

open scoped Interval Topology
open Real Filter MeasureTheory intervalIntegral

#check Function.rightLim
#check integral_log
example : Tendsto (fun ε : ℝ ↦ ∫ x in ε..1, log x) (𝓝[>] 0) (𝓝 (-1)) := by
  -- if h holds, then we can `convert` and prove that the two functions are equal on ε > 0
  suffices h : Tendsto (fun ε : ℝ ↦ -1 - ε * log ε + ε) (𝓝[>] 0) (𝓝 (-1)) by
    convert tendsto_nhdsWithin_congr ?_ h
    intro x hx
    rw [Set.mem_Ioi] at hx
    rw [integral_log_of_pos hx zero_lt_one]
    norm_num
    abel

  -- now we prove h holds! which should be simple limits
  -- I write out all the details but obviously they can be golfed
  have h1 : Tendsto (fun ε : ℝ ↦ (-1 : ℝ)) (𝓝[>] 0) (𝓝 (-1)) :=
    tendsto_const_nhds -- (x := (-1 : ℝ)) (f := 𝓝[>] 0)
  have h2 : Tendsto (fun ε : ℝ ↦ ε * log ε) (𝓝[>] 0) (𝓝 0) := by
    -- left as an exercise to the reader - jk
    -- I found this using https://leansearch.net
    -- Query: "x * log(x) -> 0 as x -> 0"
    have := tendsto_log_mul_rpow_nhds_zero zero_lt_one
    simp_rw [rpow_one, mul_comm] at this
    exact this
  have h3 : Tendsto (fun ε : ℝ ↦ ε) (𝓝[>] 0) (𝓝 0) :=
    -- we don't need the [>] part of the filter
    tendsto_nhdsWithin_of_tendsto_nhds tendsto_id

  -- note the use of dot notation here
  convert (h1.sub h2).add h3 using 2
  norm_num

[Gareth Ma]

@Stefan Kebekus :) (I also just learned about the \nhds[>] notation, it's very cool!)

[Sébastien Gouëzel]

To avoid the limiting argument and working directly on the interval, I'd try to use docs#intervalIntegral.integral_eq_sub_of_hasDerivAt_of_tendsto, together with docs#intervalIntegral.intervalIntegrable_deriv_of_nonneg to check the integrability without bothering too much.

[Gareth Ma]

I don't think it works? $x\log(x) - x$ is not continuous at $0$

[Gareth Ma]

Wait it is

[Gareth Ma]

I suggested my method above since I wasn't sure if the integral is integrable (in Mathlib?), but it works out. I also finished the proof for practice, because I'm also not familiar with measure theory things

example : ∫ x in (0 : ℝ)..1, log x = -1 := by
  rw [integral_eq_sub_of_hasDerivAt_of_tendsto (f := fun x ↦ x * log x - x) (fa := 0) (fb := -1)]
  · simp
  · simp
  · intro x hx
    norm_num at hx
    convert (hasDerivAt_mul_log hx.left.ne.symm).sub (hasDerivAt_id x) using 1
    norm_num
  · rw [← neg_neg log]
    apply IntervalIntegrable.neg
    apply intervalIntegrable_deriv_of_nonneg (g := fun x ↦ -(x * log x - x))
    · exact (continuous_mul_log.continuousOn.sub continuous_id.continuousOn).neg
    · intro x hx
      norm_num at hx
      convert ((hasDerivAt_mul_log hx.left.ne.symm).sub (hasDerivAt_id x)).neg using 1
      norm_num
    · intro x hx
      norm_num at hx
      rw [Pi.neg_apply, Left.nonneg_neg_iff]
      exact (log_nonpos_iff hx.left).mpr hx.right.le
  · have := tendsto_log_mul_rpow_nhds_zero zero_lt_one
    simp_rw [rpow_one, mul_comm] at this
    -- tendsto_nhdsWithin_of_tendsto_nhds should be under Tendsto namespace
    convert this.sub (tendsto_nhdsWithin_of_tendsto_nhds tendsto_id)
    norm_num

[Ruben Van de Velde]

Can you generalise to 0..t?

[Gareth Ma]

Yes, I was just lazy

[Gareth Ma]

Oh actually no not directly, because the strategy I'm using (I didn't look at alternate paths) is the intervalIntegrable_deriv_of_nonneg suggested above, which requires $f'(x) \geq 0$ to prove $f'(x)$ is integrable on the interval. In the proof above I wrote it as $-(-\log(x))$ then used Integrable.neg or whatever

[Gareth Ma]

But you can split it into two intervals. let me see

[Gareth Ma]

example {t : ℝ} (ht : 0 < t) : ∫ x in (0 : ℝ)..t, log x = t * log t - t := by
  rw [← integral_add_adjacent_intervals (b := 1)]
  trans (-1) + (t * log t - t + 1)
  · congr
    · -- ∫ x in 0..1, log x = -1, same proof as before
      rw [integral_eq_sub_of_hasDerivAt_of_tendsto (f := fun x ↦ x * log x - x) (fa := 0) (fb := -1)]
      · simp
      · simp
      · intro x hx
        norm_num at hx
        convert (hasDerivAt_mul_log hx.left.ne.symm).sub (hasDerivAt_id x) using 1
        norm_num
      · rw [← neg_neg log]
        apply IntervalIntegrable.neg
        apply intervalIntegrable_deriv_of_nonneg (g := fun x ↦ -(x * log x - x))
        · exact (continuous_mul_log.continuousOn.sub continuous_id.continuousOn).neg
        · intro x hx
          norm_num at hx
          convert ((hasDerivAt_mul_log hx.left.ne.symm).sub (hasDerivAt_id x)).neg using 1
          norm_num
        · intro x hx
          norm_num at hx
          rw [Pi.neg_apply, Left.nonneg_neg_iff]
          exact (log_nonpos_iff hx.left).mpr hx.right.le
      · have := tendsto_log_mul_rpow_nhds_zero zero_lt_one
        simp_rw [rpow_one, mul_comm] at this
        -- tendsto_nhdsWithin_of_tendsto_nhds should be under Tendsto namespace
        convert this.sub (tendsto_nhdsWithin_of_tendsto_nhds tendsto_id)
        norm_num
      · rw [(by simp : -1 = 1 * log 1 - 1)]
        apply tendsto_nhdsWithin_of_tendsto_nhds
        exact (continuousAt_id.mul (continuousAt_log one_ne_zero)).sub continuousAt_id
    · -- ∫ x in 1..t, log x = t * log t + 1, just use integral_log_of_pos
      rw [integral_log_of_pos zero_lt_one ht]
      norm_num
  · abel
  · -- log is integrable on [[0, 1]]
    rw [← neg_neg log]
    apply IntervalIntegrable.neg
    apply intervalIntegrable_deriv_of_nonneg (g := fun x ↦ -(x * log x - x))
    · exact (continuous_mul_log.continuousOn.sub continuous_id.continuousOn).neg
    · intro x hx
      norm_num at hx
      convert ((hasDerivAt_mul_log hx.left.ne.symm).sub (hasDerivAt_id x)).neg using 1
      norm_num
    · intro x hx
      norm_num at hx
      rw [Pi.neg_apply, Left.nonneg_neg_iff]
      exact (log_nonpos_iff hx.left).mpr hx.right.le
  · -- log is integrable on [[0, t]]
    simp [Set.mem_uIcc, ht]

[Gareth Ma]

By the way, in the proof I showed that $\log(x)$ is integrable on $[0, 1]$ (closed), but intervalIntegrable_log only shows $\log(x)$ is integrable on any interval $[a, b]$ where $0 \not\in [a, b]$ (i.e. both positive or negative). So I think there can be some strengthening

• When the measure is the volume measure!

[Gareth Ma]

I don't think it's in Mathlib

[Gareth Ma]

(deleted)

[Gareth Ma]

(deleted)

[Stefan Kebekus]

@Gareth Ma @Johan Commelin @Ruben Van de Velde @Sébastien Gouëzel Thanks again for your extremely generous help. Most likely, I would have been stuck for weeks.

[Stefan Kebekus]

@Gareth Ma Is it ok with you if I add your code to my Nevanlinna project? -- This is a project in the making, where I try to formalize the most basic theorems of Nevanlinna theory.

[Johan Commelin]

@Gareth Ma I agree that there can be some strengthening. The condition can be $0 \notin (a,b)$.

[Johan Commelin]

If you want to PR that strengthening to mathlib, that would be great. And maybe you can abstract some general "tools" from your proof into lemmas that can be useful in other places as well?

[Johan Commelin]

Because the original question by Stefan should ideally have a proof that is < 5 lines using mathlib.

[Johan Commelin]

(Preferably even a 1-liner, of course.)

[Gareth Ma]

Stefan Kebekus said:

Gareth Ma Is it ok with you if I add your code to my Nevanlinna project? -- This is a project in the making, where I try to formalize the most basic theorems of Nevanlinna theory.

Yes sure! I am already working on some other projects so I might not be too active, but (just like this thread) I can help with stuff here and there :)

[Stefan Kebekus]

@Gareth Ma Thanks!

[Gareth Ma]

Johan Commelin said:

Gareth Ma I agree that there can be some strengthening. The condition can be $0 \notin (a,b)$.

Actually you don't need any restrictions on $[a, b]$ or $(a, b)$ at all. https://gist.github.com/grhkm21/a6ea62be3dad5b0eec0602025ffd7781 (I deleted it above, it's somewhere in the edit history)

The sorry can be filled in by copying the proof above, I tried by symmetry but can't find the API

[Gareth Ma]

So theorem intervalIntegrable_log' (a b : ℝ) : IntervalIntegrable log volume a b := by holds