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

#5288

Last updated: May 16 2021 at 05:21 UTC