Zulip Chat Archive

Stream: Is there code for X?

Topic: Integrals on [0, +inf[ as limits


view this post on Zulip Floris van Doorn (Feb 23 2021 at 22:13):

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.

view this post on Zulip Floris van Doorn (Feb 23 2021 at 22:17):

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

view this post on Zulip Riccardo Brasca (Feb 23 2021 at 22:25):

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

view this post on Zulip Kevin Buzzard (Feb 23 2021 at 22:38):

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

view this post on Zulip Riccardo Brasca (Feb 23 2021 at 22:43):

I don't know Lean's measure theory library, I just mean that sin(x)x∉L1(R0)\frac{\sin(x)}{x} \not \in L^1(\mathbf{R}_{\geq 0}) for the Lebesgue measure: by definition being in L1L^1 means that the integral R0sin(x)xdx\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.

view this post on Zulip Riccardo Brasca (Feb 23 2021 at 22:47):

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

view this post on Zulip Kevin Buzzard (Feb 23 2021 at 22:52):

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

view this post on Zulip Kevin Buzzard (Feb 23 2021 at 22:52):

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

view this post on Zulip Kevin Buzzard (Feb 23 2021 at 22:53):

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

view this post on Zulip Kevin Buzzard (Feb 23 2021 at 22:54):

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

view this post on Zulip Kevin Buzzard (Feb 23 2021 at 22:54):

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

view this post on Zulip Riccardo Brasca (Feb 23 2021 at 22:56):

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,+)[0, +\infty) is an honest measure space, so we can talk about Lebesgue integrable functions on it, directly, without having to take any limit.

view this post on Zulip Kevin Buzzard (Feb 23 2021 at 22:56):

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

view this post on Zulip Kevin Buzzard (Feb 23 2021 at 22:57):

I guess it's the same phenomenon

view this post on Zulip Heather Macbeth (Feb 23 2021 at 22:57):

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\sin(x)/x, yes!

view this post on Zulip Kevin Buzzard (Feb 23 2021 at 22:58):

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

view this post on Zulip Heather Macbeth (Feb 23 2021 at 22:58):

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

view this post on Zulip Kevin Buzzard (Feb 23 2021 at 22:59):

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

view this post on Zulip Kevin Buzzard (Feb 23 2021 at 23:00):

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

view this post on Zulip Riccardo Brasca (Feb 23 2021 at 23:23):

I believe that one of the reasons to define L1L^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 (1)nn=log(2)\sum \frac{(-1)^n}{n} = -\log(2) as an integral in 1\ell^1 this is very weird: think of this as the integral of a simple function, now rearrange the points to have sum 3737. You have changed the function, but from a measure theory point of view all the points are the same (the measure space is N\mathbf{N} with the counting measure) so the new function should have the same integral.

view this post on Zulip Kevin Buzzard (Feb 24 2021 at 00:01):

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

view this post on Zulip Anatole Dedecker (Feb 24 2021 at 09:39):

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 f\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).

view this post on Zulip Kevin Buzzard (Feb 24 2021 at 10:28):

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

view this post on Zulip Anatole Dedecker (Feb 26 2021 at 23:05):

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

view this post on Zulip Anatole Dedecker (Mar 14 2021 at 21:58):

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) ?

view this post on Zulip Rémy Degenne (Mar 14 2021 at 22:07):

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.

view this post on Zulip Rémy Degenne (Mar 14 2021 at 22:09):

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


Last updated: May 19 2021 at 02:10 UTC