prod of inner product spaces

Stream: maths

[Moritz Doll]

Hi, I was trying to prove some things about the graph of linear_pmaps in inner product spaces, but there seems to be quite a serious issue with the definition of the norm of the product: if I see it correctly it is at the moment impossible to define an instance inner_product_space 𝕜 (E × F) since the norm is the $L^\infty$ norm and not the $L^2$ norm. On the other side I think there were very good reasons to take the maximum and I think I saw some discussion on zulip about this, but I could not find it.

[Moritz Doll]

the 'bad' definition is this one docs#prod.seminormed_add_comm_group

[Yaël Dillies]

You should use docs#pi_Lp, not docs#prod.

[Yaël Dillies]

I would guess docs#pi_Lp.inner_product_space.

[Eric Wieser]

This maybe raises the question of whether defining prod_Lp is worth the boilerplate it comes with

[Heather Macbeth]

One previous discussion where this gap was observed:
https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Fubini's.20for.20fin.202.20-.3E.20R/near/222198621

I don't think we could outright switch to the $L^2$ definition, because the square root function is defined much later in the library than the max function.

As Yaël says, so far people have mostly been getting along by using pi_Lp (fin 2). But I would be mildly in favour of having prod_Lp if you have the energy to implement it!

[Jireh Loreaux]

On a tangentially related topic, just FYI, I am currently implementing the equivalence between lp and pi_Lp. Should be ready in a day or two once I have time to work on it again.

[Moritz Doll]

I guess will not do it in the near future, except if I really need it. I would not be happy using docs#pi_Lp that feels rather unnatural to me. For the definition of the adjoint there is a construction that avoids using the graph, so I don't need products of Hilbert spaces.

[Violeta Hernández]

What about defining prod_Lp as pi_Lp (fin 2)?

[Violeta Hernández]

Or perhaps pi_Lp bool, as I imagine that this is the canonical 2-element type

[Anatole Dedecker]

I think prod_Lp would be a natural thing to have, and imo it would be best to define it as a type alias over the true prod and then pull back all the structure from pi_Lp

[Moritz Doll]

Heather Macbeth said:

One previous discussion where this gap was observed:
https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Fubini's.20for.20fin.202.20-.3E.20R/near/222198621

I don't think we could outright switch to the $L^2$ definition, because the square root function is defined much later in the library than the max function.

As Yaël says, so far people have mostly been getting along by using pi_Lp (fin 2). But I would be mildly in favour of having prod_Lp if you have the energy to implement it!

Actually it is possible to include data.real.sqrt in analysis.normed.group.basic: https://github.com/leanprover-community/mathlib/blob/mcdoll/adjoint/src/analysis/normed/group/basic.lean

[Heather Macbeth]

But it would need to be even earlier, right? We have e.g. docs#prod.metric_space_max

[Yaël Dillies]

Do NOT change the default distance on the product. This is a very general thing and it is personally crucial to me right now that balls are cubes for proving that upper sets in ι → ℝ are measurable.

[Moritz Doll]

Even if we wanted to do that, I don't think we would find anyone volunteering for that insane amount of work

[Yaël Dillies]

Actually, can pi_Lp even represent the max norm? It takes in a real, not a ennreal.

[Moritz Doll]

Heather, you are of course right. there are cyclic import if one wants to import data.real.sqrt in the metric space file.

[Yaël Dillies]

Should pi_Lp be generalized to take in ereal, so that we can state results about the infinity norm homogeneously with the other norms?

[Moritz Doll]

There might be a point to that, since right now I think it would be impossible to state interpolation results in good way.

[Yaël Dillies]

and maybe mean inequalities?

[Eric Wieser]

Do you definitely mean ereal and not ennreal?

[Yaël Dillies]

Yes, because currently docs#pi_Lp takes in a docs#real, but maybe it could really be restricted to nnreal.

[Jireh Loreaux]

I was thinking it could be nice if it took an ennreal. Then it would match lp. This should also make the equivalence significantly simpler.

[Jireh Loreaux]

I'm going to undertake the change of switching to ennreal, unless someone objects, but there seemed to be enough :thumbs_up: to do it.

[Heather Macbeth]

ping @Sebastien Gouezel, who wrote docs#pi_Lp

[Sebastien Gouezel]

I think it is a very good idea to refactor pi_Lp to use an ennreal, and also to define prod_Lp.

[Jireh Loreaux]

@Heather Macbeth , @Sebastien Gouezel the refactor of pi_Lp is ready: #15833 (modulo moving a few lemmas at the top of the file to appropriate places). I thought you might want to be the one(s) to take a look since you are the authors of pi_Lp and lp.

[Jireh Loreaux]

@Alex Kontorovich just asked for the inner product on a prod. Is anyone implementing it currently? I don't think it should be too hard: just define a type synonym for prod and a map from there into pi_Lp (fin 2) and pull all the structure back. Actually, now that I think about it, does that pullback actually make the product, uniform and bornological structures match those of prod definitionally? Probably not?

[Anatole Dedecker]

No but if forgetful inheritance is setup correctly that shouldn’t be too much of a problem

[Yaël Dillies]

You can also just do it by hand and that won't be too hard. I've been waiting to have time to pull it off myself but that didn't happen yet :slight_frown:

[Jireh Loreaux]

I mean, it's not a terrible amount of work, but it would be annoying to do it twice (once for pi_Lp and once for prod_Lp).

[Yaël Dillies]

Eh, we treat pi and prod separately everywhere else.

[Jireh Loreaux]

Yeah, but with pi_Lp you have to (or rather, prefer to) do all these shenanigans to make the structures determined by the metric structure agree definitionally with the ones that exist on the underlying Π-type. We would want to do the same with prod_Lp. It would be nice if we can just get it for free instead of duplicating the work. I believe this is why everyone has been loathe to implement it.