continuous implies integrable

Stream: Is there code for X?

[Heather Macbeth]

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]

There can't be continuous_on.measurable because a function can be very bad outside of s.

[Yury G. Kudryashov]

So, continuous_on.integrable_on should assume measurable.

[Yury G. Kudryashov]

And we have continuous_on.integrable_on_compact

[Yury G. Kudryashov]

Unfortunately, integrals are defined so that f has to be measurable everywhere.

[Heather Macbeth]

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

[Heather Macbeth]

What about continuous.interval_integrable, the lemma I wrote?

[Yury G. Kudryashov]

Should be easy to prove using continuous_on.integrable_on_compact.

[Heather Macbeth]

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

[Yury G. Kudryashov]

Currently ∫ x in s, f x ∂μ is defined as ∫ x, f x ∂(μ.restrict s), not ∫ x, set.indicator s f ∂μ.

[Yury G. Kudryashov]

Possibly, this was a bad design choice (I changed it from indicator some time ago).

[Heather Macbeth]

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]

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

[Yury G. Kudryashov]

You can do interval_integrable u μ a b provided that [locally_finite_measure μ].

[Yury G. Kudryashov]

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

[Heather Macbeth]

#5288