Integrals on [0, +inf[ as limits

Stream: Is there code for X?

[Floris van Doorn]

I think to do this you need to assume that f is integrable on all of Ico 0, and it might be false if you only assume that for all x it is integrable on Icc 0 x. If you assume that it should follow without too much trouble from docs#measure_theory.tendsto_integral_of_dominated_convergence.

[Floris van Doorn]

Take bound := |f| (or (Ico 0).indicator |f|) and F n := (Ioc 0 n).indicator f

[Riccardo Brasca]

The function $f(x) =\frac{\sin(x)}{x}$ is not integrable on $[0, + \infty)$, but $\lim_{c \to \infty} \int_0^c f(x) dx = \frac{\pi}{2}$.

[Kevin Buzzard]

What's the definition of integrable on [0,infty)? It's been a long time! Is 1/floor(x+1) also problematic?

[Riccardo Brasca]

I don't know Lean's measure theory library, I just mean that $\frac{\sin(x)}{x} \not \in L^1(\mathbf{R}_{\geq 0})$ for the Lebesgue measure: by definition being in $L^1$ means that the integral $\int_{\mathbf{R}_{\geq 0}} \left | \frac{\sin(x)}{x}\right | dx$ is finite. And the integral of a positive function is defined using simple functions.

[Riccardo Brasca]

So yes, 1/floor(x+1) is not integrable. The difference is that $\frac{\sin(x)}{x}$ has a well defined improper Riemann integral, that equals the limit by definition.

[Kevin Buzzard]

Oh I'm an idiot, I meant to say (-1)^(floor(x+1))/floor(x+1)

[Kevin Buzzard]

I'm trying to simulate an alternating sum of 1/n

[Kevin Buzzard]

I'm pretty sure that I was taught that the integral of this from 0 to infinity existed when we were doing Riemann integral, and I didn't pay attention in Lebesgue integral class

[Kevin Buzzard]

I just had the impression that Riemann integrable implied Lebesgue integrable but now I'm not so sure

[Kevin Buzzard]

It was Lebesgue integral class that convinced me I didn't want to be an analyst

[Riccardo Brasca]

The point is that over an unbounded interval there is no direct notion of Riemann integral: we have to take the limit even in the definition. But $[0, +\infty)$ is an honest measure space, so we can talk about Lebesgue integrable functions on it, directly, without having to take any limit.

[Kevin Buzzard]

I was very confused about some of the lemmas in Lean's tsum namespace until I realised that sum of (-1)^n/n was not summable, again I was told that it had a sum

[Kevin Buzzard]

I guess it's the same phenomenon

[Heather Macbeth]

Kevin Buzzard said:

Oh I'm an idiot, I meant to say (-1)^(floor(x+1))/floor(x+1)

I think this works in the same way as $\sin(x)/x$, yes!

[Kevin Buzzard]

So Riemann integrable but not Lebesgue integrable, like the sum above is convergent but not absolutely convergent

[Heather Macbeth]

I too like all my real analysis counterexamples to be constructed from $(-1)^n$ and floor, that way you can use them honestly in your elementary real analysis class without constructing the trigonometric functions.

[Kevin Buzzard]

I had not really realised that convergent but not absolutely convergent things were somehow rejected -- I had imagined that they had some sort of use

[Kevin Buzzard]

They were useful for exam questions in my Riemann integral course but I didn't take the Lebesgue integral exam

[Riccardo Brasca]

I believe that one of the reasons to define $L^1$ in this way is that we want it to be a very well behaved space (aka a Banach space). The situation is completely analogous to that of series, we can play with convergent series and doing a lot of interesting exercises, but to set up a nice theory we need absolutely convergent series.

Even intuitively, if you look at $\sum \frac{(-1)^n}{n} = -\log(2)$ as an integral in $\ell^1$ this is very weird: think of this as the integral of a simple function, now rearrange the points to have sum $37$. You have changed the function, but from a measure theory point of view all the points are the same (the measure space is $\mathbf{N}$ with the counting measure) so the new function should have the same integral.

[Kevin Buzzard]

That's a really nice way of looking at it -- thanks!

[Anatole Dedecker]

Thanks to all of you ! As I said I haven't followed any course in measure theory, so it really helps me to get the philosophy. If I understand correctly, the lemma is true if f is integrable, but that means having to compute the integral of $\Vert f\Vert$. Tell me if 'm wrong, but there should be a way to throw out that assumption if f is nonnegative, right ? I think so because I managed to prove the following :

lemma lintegral_eq_of_tendsto (φ : ℕ → set α) (hφ₁ : ∀ x, ∀ᶠ n in at_top, x ∈ φ n)
  (hφ₂ : monotone φ) (hφ₃ : ∀ n, measurable_set $ φ n) (f : α → ℝ≥0∞) (I : ℝ≥0∞)
  (hfm : measurable f) (h : tendsto (λ n, ∫⁻ x in φ n, f x ∂μ) at_top (𝓝 I)) :
∫⁻ x, f x ∂μ = I := sorry

I'm currently trying to deduce form that a similar lemma about nonnegative functions to the real numbers (where I would be a real number too).

[Kevin Buzzard]

If f is nonnegative then all these concerns above should be irrelevant, yes

[Anatole Dedecker]

FYI, after quite a bit of work, I now have proofs of the following :

lemma integral_eq_of_tendsto_integral {φ : ℕ → set α} (hφ₁ : ∀ x, ∀ᶠ n in at_top, x ∈ φ n)
  (hφ₂ : monotone φ) (hφ₃ : ∀ n, measurable_set $ φ n) {f : α → ℝ} (I : ℝ)
  (hfm : measurable f) (hfi : integrable f μ)
  (h : tendsto (λ n, ∫ x in φ n, f x ∂μ) at_top (𝓝 I)) :
  ∫ x, f x ∂μ = I := sorry

lemma integral_eq_of_tendsto_integral_of_nonneg_ae {φ : ℕ → set α} (hφ₁ : ∀ x, ∀ᶠ n in at_top, x ∈ φ n)
  (hφ₂ : monotone φ) (hφ₃ : ∀ n, measurable_set $ φ n) {f : α → ℝ} (I : ℝ)
  (hf : 0 ≤ᵐ[μ] f) (hfm : measurable f) (hfi : ∀ n, integrable_on f (φ n) μ)
  (h : tendsto (λ n, ∫ x in φ n, f x ∂μ) at_top (𝓝 I)) :
  ∫ x, f x ∂μ = I := sorry

[Anatole Dedecker]

I started to clean and generalize this code in order to make a PR out of it. You can see the current version at https://github.com/ADedecker/gauss/blob/master/src/integral_limits.lean

I was stuck when trying to generalize those results for f : α → Ewith all the assumptions on E for the integral to be defined. The problems come from my initial roadmap, which was basically "prove everything for lintegrals, and then use docs#integral_eq_lintegral_max_sub_lintegral_min to deduce eveything I need". Of course, this doesn't work for a general E, so for now I'm stuck to ℝ starting from https://github.com/ADedecker/gauss/blob/d0540faf76483cc13bd031364ddbd799ed3a68c7/src/integral_limits.lean#L164

Is there any way I could solve this without having to go back to the procedure described in bochner_integration.lean (going back to simple functions and so on) ?

[Rémy Degenne]

The lemma integrable.induction (in set_integral.lean) may help. It is a kind of fast track through the "simple function and so on" procedure.
I have not looked at what you want to prove though. It may not apply.

[Rémy Degenne]

See integral_comp_comm in the same file for an example of its use.