## Stream: Is there code for X?

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

#### 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.

#### 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

#### Riccardo Brasca (Feb 23 2021 at 22:25):

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

#### Riccardo Brasca (Feb 23 2021 at 22:43):

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 (Feb 23 2021 at 22:47):

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 (Feb 23 2021 at 22:52):

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

#### Kevin Buzzard (Feb 23 2021 at 22:52):

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

#### 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

#### 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

#### Kevin Buzzard (Feb 23 2021 at 22:54):

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

#### 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, +\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 (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

#### Kevin Buzzard (Feb 23 2021 at 22:57):

I guess it's the same phenomenon

#### 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$, yes!

#### 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

#### Heather Macbeth (Feb 23 2021 at 22:58):

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 (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

#### 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

#### Riccardo Brasca (Feb 23 2021 at 23:23):

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 (Feb 24 2021 at 00:01):

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

#### 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 $\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 (Feb 24 2021 at 10:28): If f is nonnegative then all these concerns above should be irrelevant, yes #### 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


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

#### 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.

#### 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