Simple functions in Lp

Stream: maths

[Heather Macbeth]

I would be glad of some tips for formalizing an argument for L^p, in which a main step is "approximation by simple functions" (@Rémy Degenne @Sebastien Gouezel @Yury G. Kudryashov)

We can prove facts about L^1 by approximation by simple functions, using docs#measure_theory.L1.simple_func.dense_embedding. (And indeed the Bochner integral is constructed this way.). But if I understand correctly, we don't yet have a similar result for L^p, nor do we have the underlying results such as docs#measure_theory.simple_func.integrable_approx_on_univ in the L^p setting. Is that right? Any advice about how to implement it?

(I want to prove that continuous functions are dense in L^p, and I'm not so far from being able to show that continuous functions L^p-approximate simple functions: branch#continuous_dense_lp.)

[Heather Macbeth]

In particular, I think I could rewrite the file measure_theory.simple_func_dense so that every lemma from docs#tendsto_approx_on_L1_edist downwards is stated for L^p, not L^1; would this be a good change?

[Sebastien Gouezel]

I think that's a very good idea. I'd be interested in hearing the thoughts of @Rémy Degenne , since he knows this mathlib area extremely well.

[Rémy Degenne]

I think that generalizing the approximation results is a good idea, and is probably the best way of getting what you want. The main reason that all those results exist for L1 and not Lp seem to be that L1 predates the definition of the Lp spaces in mathlib. If you are willing to work on making all those statements more general, please go ahead, and thank you very much!

[Rémy Degenne]

The lemma docs#measure_theory.integrable.induction is also often useful to transfer a result from simple functions to L1 functions.

[Heather Macbeth]

OK great, let me see what I can do!

Is anyone particularly attached to having certain facts about integration in normed groups stated in terms of edist? I am thinking of

• docs#measure_theory.simple_func.tendsto_approx_on_L1_edist
• docs#measure_theory.simple_func.tendsto_approx_on_univ_L1_edist
• docs#measure_theory.tendsto_integral_of_L1

and had in mind to change it to a phrasing in terms of nnnorm.

[Rémy Degenne]

Since using nnnorm is the standard way to write statements about L^p functions (like the norm in L^p is written with nnnorm and not edist), I think that changing them is a good idea. But I did not write nor use those lemmas, so there might be a good reason for using edist that I don't see. You'll see what breaks!

[Sebastien Gouezel]

I think it's a historical artefact, and that this change would definitely be a good move.

[Heather Macbeth]

Thanks for the advice! I have made a first pass in #8114, rewriting the file measure_theory/simple_func_dense completely but leaving other files, in particular measure_theory/bochner_integral, essentially untouched. This gives a kind of bare-hands approximation result, without yet the more abstract versions.