[Merged by Bors] - feat(measure_theory/l2_space): L2 is an inner product space

[RemyDegenne]

If E is an inner product space, then so is Lp E 2 µ, with inner product being the integral of the inner products between function values.

---

• depends on: [Merged by Bors] - feat(data/real/{nnreal,ennreal}): add (e)nnreal.of_real_bit0/bit1 #6617
• depends on: [Merged by Bors] - feat(measure_theory/lp_space): add snorm_norm_rpow #6619
• depends on: [Merged by Bors] - feat(data/complex/is_R_or_C): add linear maps for is_R_or_C.re, im, conj and of_real #6621
• depends on: [Merged by Bors] - feat(measure_theory/bochner_integration): extend the integral_smul lemmas #6654

While I could prove this for R, I wanted to do it for is_R_or_C and I have two sorry for which I could use some help. The lemmas I am missing are integral_coe and integral_conj, stating respectively that we can switch coe (from R to an is_R_or_C) and integral, or is_R_or_C.conj and integral.

This is very much WIP: I will PR most of the supporting results separately (the lemmas outside of l2_space.lean), move some results to other files, and golf the main proofs. I put this up as a PR to advertise my need for integral_coe and integral_conj. If you make a proof of either one, please feel free to push to the branch!

[RemyDegenne]

I think that I found a nice way of obtaining the two missing lemmas: I proved results about the integral of a composition with a continuous linear map.

[sgouezel]

I am just working on this. Composition with continuous linear maps is already there, in set_integral.lean, but some plumbing is required when the function is not integrable. Let me push what I have currently.

[sgouezel]

In what I have merged, the lemma linear_isometry.integral_comp_comm (in set_integral.lean) says that the integral is equivariant with respect to composition with a linear isometry, without integrability assumptions.

[sgouezel]

I am not touching the files any more, so you can fix things the way you prefer.

[PatrickMassot]

You are really ploughing through the function spaces part of
https://leanprover-community.github.io/undergrad_todo.html
@PatrickMassot, can we count

Espaces de Hilbert
... Cas des espaces ℓ² et L².

as being completed by this PR?

I would say yes then. It's a bit tricky to know where the link should go if we don't have a definition for Hilbert spaces but only the combination of inner_product_space and complete_space (we have the same issue for Banach spaces).

[hrmacbeth]

For the Banach space C^0, we say,

normed space of bounded continuous functions (<link 1>), its completeness (<link 2>)

We could do the same here:

inner product spaces ℓ² and L² (<link 1>), their completeness (<link 2>)

[RemyDegenne]

Where should I add those comments and links?

[hrmacbeth]

Patrick is the ultimate arbiter of the undergrad list (docs/undergrad.yaml), but I would suggest, replace the current line 434 in the "Hilbert spaces" section,

    $l^2$ and $L^2$ cases:

with two lines

    inner product spaces $l^2$ and $L^2$: <your_theorem>
    their completeness: <your_other_theorem>

Thanks!

[PatrickMassot]

Patrick is the ultimate arbiter of the undergrad list (docs/undergrad.yaml)

That's not true actually. I started this list because I thought it was important. And, because I had no better idea, I based it on a French document so I can help with translation. But this is a common good. Everybody on the maintainer team should feel free to edit it. And your suggestions about the topic at hand sounds perfect to me.

[sgouezel]

LGTM

[sgouezel]

bors r+
Thanks!

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests