Lp space

Stream: maths

[Heather Macbeth]

We have two versions of Lp space in mathlib already, docs#pi_Lp and docs#measure_theory.Lp. I propose to add a third version! This would be sort of like the standard $\ell^p$ but more general. I'd like people to sanity-check that this is really necessary, and I'd like to decide on a naming scheme. @Rémy Degenne @Sebastien Gouezel @Yury G. Kudryashov @Patrick Massot

Currently, pi_Lp puts the norm (∑ a, ∥f a∥ ^ p) ^ (1 / p) on Π a : α, E a for α finite, and measure_theory.Lp puts the norm (∫ a, ∥f a∥ ^ p ∂μ) ^ (1 / p) on the subgroup of α →ₘ[μ] E for which that norm is finite, for α a measure space. My proposed new construction ℓp (see branch#hilbert-sum, still with some sorries) would put the norm (∑' a, ∥f a∥ ^ p) ^ (1 / p) on the subgroup of Π a : α, E a for which that norm is finite.

This is more general than measure_theory.Lp in that it allows the target space E a to vary with a. It's less general than measure_theory.Lp in that it permits only the counting measure on the domain α, not an arbitrary measure. I don't think the constructions can be combined, because there's no notion of measurability for the space Π a : α, E a.

The construction is more general than pi_Lp because α is permitted to be allowed to be infinite, but since the pi_Lp construction is more elementary I think that should continue to exist, too.

So, do others agree to add this new version of Lp? (My intended application is for the spectral theorem: I want to express a Hilbert space as the ℓ2 (in this sense) of the eigenspaces of a compact operator on that space). How should we name it, if so?

[Jireh Loreaux]

For however much my opinion counts, I agree we should have the third version (I'm all for keeping the finite one unless it would mean lots of code duplication). For naming, there's ell_p although I really don't love that.

One thing to note, it's more work (read: a long way off), but you can get the spectral theorem from the Borel functional calculus and for compact operators you can show the measure is purely atomic, which corresponds to a basis for diagonalization. It may make sense to just have both constructions eventually.

[Patrick Massot]

We clearly need $\ell^p$ so only the naming question really exists. I think Jireh's suggestion could be use, but l_p seems to be available as well.

[Yury G. Kudryashov]

One more reason to preserve pi_Lp: it has the same uniform_space structure as the usual pi type. This won't be true for the new space.

[Heather Macbeth]

PR'd as #11015, leaving the naming question unresolved for now.

[Oliver Nash]

So the gap #11015 fills is that it allows us to adorn an infinite dependent product with an L^p structure, since we can already do this for finite dependent products using docs#pi_LP and infinite non-dependent products using docs#measure_theory.Lp (with the counting measure). I agree this is worth having but I'd be curious to see an example.

[Heather Macbeth]

@Oliver Nash Given a self-adjoint compact operator $T$ on a separable Hilbert space $E$, there is a unitary isomorphism from $E$ to the lp 2 of the eigenspaces of $T$ ....

[Oliver Nash]

Oh right of course. Nice!

[Oliver Nash]

Aaaaaand what will we do with the non-separable case ? :wink:

[Heather Macbeth]

It's nearly the same, it's the direct sum of the kernel with the lp 2 of the nonzero eigenspaces.

[Jireh Loreaux]

also ultraproducts

[Oliver Nash]

That's not really a serious question! I'm busy trying to golf one of your proofs :-)

[Heather Macbeth]

Actually, maybe I don't need the case distinction there!