# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: continuous implies integrable

#### Heather Macbeth (Dec 09 2020 at 01:41):

Where are we at in terms of lemmas linking continuity to integrability? I found docs#continuous.integrable_on_compact , but couldn't find variants such as,

```
lemma continuous.interval_integrable {u : ℝ → ℝ} (hu : continuous u) (a b : ℝ) :
interval_integrable u measure_theory.measure_space.volume a b :=
begin
split;
{ refine measure_theory.integrable_on.mono_set _ Ioc_subset_Icc_self,
apply hu.integrable_on_compact compact_Icc,
exact real.locally_finite_volume },
end
```

Also, I tried writing a `continuous_on`

variant, but did not find `continuous_on.measurable`

(although we do have docs#continuous.measurable).

Are these things indeed missing? Let me know if I overlooked something or if there's a better way. @Yury G. Kudryashov

#### Yury G. Kudryashov (Dec 09 2020 at 01:57):

There can't be `continuous_on.measurable`

because a function can be very bad outside of `s`

.

#### Yury G. Kudryashov (Dec 09 2020 at 01:58):

So, `continuous_on.integrable_on`

should assume `measurable`

.

#### Yury G. Kudryashov (Dec 09 2020 at 01:58):

And we have `continuous_on.integrable_on_compact`

#### Yury G. Kudryashov (Dec 09 2020 at 01:59):

Unfortunately, integrals are defined so that `f`

has to be measurable everywhere.

#### Heather Macbeth (Dec 09 2020 at 01:59):

Ah, I see, there is no relative version of `measurable`

.

#### Heather Macbeth (Dec 09 2020 at 02:00):

What about `continuous.interval_integrable`

, the lemma I wrote?

#### Yury G. Kudryashov (Dec 09 2020 at 02:01):

Should be easy to prove using `continuous_on.integrable_on_compact`

.

#### Heather Macbeth (Dec 09 2020 at 02:02):

Indeed I proved it above ... just wanted to know if I should PR it :)

#### Yury G. Kudryashov (Dec 09 2020 at 02:02):

Currently `∫ x in s, f x ∂μ`

is defined as `∫ x, f x ∂(μ.restrict s)`

, not `∫ x, set.indicator s f ∂μ`

.

#### Yury G. Kudryashov (Dec 09 2020 at 02:03):

Possibly, this was a bad design choice (I changed it from `indicator`

some time ago).

#### Heather Macbeth (Dec 09 2020 at 02:05):

I don't follow, could you please explain? Are you saying the statement I wrote above

```
interval_integrable u measure_theory.measure_space.volume a b
```

is not what it should be?

#### Heather Macbeth (Dec 09 2020 at 02:09):

Oh, never mind, I guess you are explaining why there is no natural relative version of `measurable`

.

#### Yury G. Kudryashov (Dec 09 2020 at 02:13):

You can do `interval_integrable u μ a b`

provided that `[locally_finite_measure μ]`

.

#### Yury G. Kudryashov (Dec 09 2020 at 02:20):

Then it'll work for, e.g., probability measures on `\R`

.

#### Heather Macbeth (Dec 09 2020 at 02:42):

Last updated: May 16 2021 at 05:21 UTC