ae measurable condition

Stream: Is there code for X?

[Oliver Nash]

I think we are missing the following result:

import measure_theory.integral.interval_integral

open set measure_theory

variables {E : Type*} [normed_group E] [normed_space ℝ E]
variables {a b : ℝ} {μ : measure ℝ} {f : ℝ → ℝ} {g : ℝ → E}

lemma interval_integrable.smul_continuous_on
  (hf : interval_integrable f μ a b) (hg : continuous_on g (interval a b)) :
  interval_integrable (λ x, f x • g x) μ a b :=
sorry

and I believe it should be easy to obtain from:

lemma measure_theory.ae_strongly_measurable.smul_continuous_on
  (hf : ae_strongly_measurable f $ μ.restrict $ interval_oc a b) (hg : continuous_on g (interval a b)) :
  ae_strongly_measurable (λ x, f x • g x) $ μ.restrict $ interval_oc a b :=
sorry

(though perhaps there are other/better proofs). I haven't looked much into these corners of Mathlib yet. Are either of these results easy for the experts?

[Bhavik Mehta]

The second goal is easy:

lemma measure_theory.ae_strongly_measurable.smul_continuous_on
  (hf : ae_strongly_measurable f (μ.restrict (interval_oc a b)))
  (hg : continuous_on g (interval a b)) :
  ae_strongly_measurable (λ x, f x • g x) (μ.restrict (interval_oc a b)) :=
hf.smul ((hg.mono interval_oc_subset_interval).ae_strongly_measurable measurable_set_interval_oc)

The first one looks familiar to me - I think I've done something similar before - but I can't figure it out right now

[Oliver Nash]

Wow, thanks! I have a proof somewhere that reduces the first proof to the one you've just proved so I have everything I need now. I'll try to come back to this later today and put your work to good use.

[Bhavik Mehta]

Ah I remember now - the bit that's left is to use hg to show g is bounded, and from there deduce that f * g has finite integral. Out of interest do you know if your way for the remainder is the same?

[Oliver Nash]

I believe it's slightly different. You can see it here: https://github.com/leanprover-community/sphere-eversion/commit/abc10fae23eac32b5e1e4bb5a21c3508bd5c81a3#diff-ad9f3bdd847db104518f135aab4380a57eec97691051439cef91a5e96dc02f11L28

[Oliver Nash]

In other words, it uses https://github.com/leanprover-community/sphere-eversion/blob/c55336903ba5ca5b5e9a678d95250ea0edf37e98/src/to_mathlib/measure_theory/interval_integral.lean#L43 to reduce to docs#interval_integrable.mul_continuous_on

[Bhavik Mehta]

Ah right! I think that points out a hole - there's docs#interval_integrable.mul_continuous_on but no version for integrable_on

[Oliver Nash]

Yes, I noted that also.

[Bhavik Mehta]

Oh, I'm wrong again docs#integrable_on.mul_continuous_on_of_subset

[Oliver Nash]

We have migrated a bit of stuff out of the SE repo to Mathlib recently and I'm hoping to do a bit more next week. Filling various such holes should happen as part of such an effort.

[Bhavik Mehta]

To be clear I don't think I'm an expert in this part of mathlib, I've just been using it a lot recently for the unit fractions project!

[Oliver Nash]

From where I'm sitting, you're an expert!

[Oliver Nash]

It's pleasing to learn that two efforts as distant as the Unit Fractions and Sphere Eversion projects are helping each other in this way. It's only a small example but it's still a good example of the synergy of our Monolithic Mathlib philosophy.

[Floris van Doorn]

I'm using very similar lemmas for the convolution PR (#13540), but I'm doing everything with continuous bilinear maps instead of mul/smul. Which makes me realize I should probably extract those lemmas and put them in different files.