Zulip Chat Archive

Stream: Is there code for X?

Topic: continuous implies integrable


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Dec 09 2020 at 01:58):

So, continuous_on.integrable_on should assume measurable.

view this post on Zulip Yury G. Kudryashov (Dec 09 2020 at 01:58):

And we have continuous_on.integrable_on_compact

view this post on Zulip Yury G. Kudryashov (Dec 09 2020 at 01:59):

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

view this post on Zulip Heather Macbeth (Dec 09 2020 at 01:59):

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

view this post on Zulip Heather Macbeth (Dec 09 2020 at 02:00):

What about continuous.interval_integrable, the lemma I wrote?

view this post on Zulip Yury G. Kudryashov (Dec 09 2020 at 02:01):

Should be easy to prove using continuous_on.integrable_on_compact.

view this post on Zulip Heather Macbeth (Dec 09 2020 at 02:02):

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

view this post on Zulip 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 ∂μ.

view this post on Zulip Yury G. Kudryashov (Dec 09 2020 at 02:03):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Dec 09 2020 at 02:13):

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

view this post on Zulip Yury G. Kudryashov (Dec 09 2020 at 02:20):

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

view this post on Zulip Heather Macbeth (Dec 09 2020 at 02:42):

#5288


Last updated: May 16 2021 at 05:21 UTC