Inner product space on α × β

Stream: Is there code for X?

[Yaël Dillies]

Am I blind or do we not have the inner_product_space (α × β) instance?

[Yury G. Kudryashov]

You need a def l2_prod, because the default norm on the product is the maximum.

[Frédéric Dupuis]

Is pi_Lp.inner_product_space the instance you're looking for?

[Heather Macbeth]

Frédéric Dupuis said:

Is pi_Lp.inner_product_space the instance you're looking for?

Yes, this would be the usual workaround.

[Eric Wieser]

Should we have prod_Lp to match pi_Lp?

[Heather Macbeth]

Let's wait until (if ever) it's needed for something -- the definition of the metric/normed space instances on pi_Lp requires several little inequality proofs which it would be sad to have to repeat. See also
https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Fubini's.20for.20fin.202.20-.3E.20R/near/222194513

[Yury G. Kudryashov]

You can use equivalence to Π b : bool, cond (ulift α) (ulift β) to get all structures (probably with poor definitional equalities).

[Alex Kontorovich]

Just checking if there were any changes in mathlib since this discussion? What's the easiest way to make an inner_product_space on E₁ × E₂, where both are themselves inner product spaces (with the inner form on the product being the direct sum of the two forms)?

[Jireh Loreaux]

There was this recent discussion: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/prod.20of.20inner.20product.20spaces/near/291488589

This resulted in #15833, but that's a refactor of pi_Lp, not a prod_Lp type (but any prod_Lp should follow the refactor).

[Jireh Loreaux]

So, at this moment, I think you can use pi_Lp 2 E in the finite case, where E : fin 2 → Type* such that E 0 = E₁ and E 1 = E₂. However, if no one else does it, I'll probably get around to making this prod_Lp type. (No promises right now though.)

[Alex Kontorovich]

Ah, thanks. I can't seem to even get this much started... Do I have the syntax wrong somehow?

import data.real.basic
import analysis.inner_product_space.basic

variables (E₁ E₂ : Type*) [inner_product_space ℝ E₁] [inner_product_space ℝ E₂]

@[derive [add_comm_group, module ℝ]]def new_space := E₁ × E₂

instance : inner_product_space ℝ new_space := sorry

[Jireh Loreaux]

Your new_space takes E₁ and E₂ as explicit arguments, so instance : inner_product_space ℝ (new_space E₁ E₂) := sorry is valid

[Jireh Loreaux]

You can see this in the error message:

type mismatch at application
  inner_product_space ℝ new_space
term
  new_space
has type
  Π (E₁ : Type ?) (E₂ : Type ?) [_inst_1 : inner_product_space ℝ E₁] [_inst_2 : inner_product_space ℝ E₂],
    Type (max ? ?) : Type (max (?+1) (?+1) ? ? (?+1) (?+1))
but is expected to have type
  Type ? : Type (?+1)

So, the issue it's having is with new_space, and it says : "hey this thing isn't a type! It's a thing that takes two types which are inner_product_spaces and it returns another type!"

[Alex Kontorovich]

Ah, thanks! I'm an idiot...

[Alex Kontorovich]

Hmm any hint on how to get that E : fin 2 → Type* to work? I tried this and it's not working... Thanks!

have := pi_Lp 2 (![E₁, E₂] : (fin 2) → (Type*)),

[Jireh Loreaux]

The problem here is that your E₁ and E₂ need to live in a common type universe because E : fin 2 → Type* really means E : fin 2 → Type u (polymorphic over the universe parameter u). But you declared (E₁ E₂ : Type*), which really means (E₁ : Type u) and (E₂ : Type v) for some universes u and v, but then your ![E₁, E₂] 0 : Type u but ![E₁, E₂] 1 : Type v which doesn't work. This works:

import data.real.basic
import analysis.inner_product_space.basic
import analysis.normed_space.pi_Lp

universes u

variables (E₁ E₂ : Type u) [inner_product_space ℝ E₁] [inner_product_space ℝ E₂]

@[derive [add_comm_group, module ℝ]]def new_space := E₁ × E₂

instance : inner_product_space ℝ (new_space E₁ E₂) :=
have foo : Type u := pi_Lp 2 (![E₁, E₂] : (fin 2 → Type u)),
sorry

[Jireh Loreaux]

However, if you're really going to do this, I highly suggest the method described in the other thread of pulling back the structure from pi_Lp. It's much easier.

[Alex Kontorovich]

Thanks! I am trying to pull back the structure, but I guess I'm doing it wrong...? (And how would I do it if the two spaces are really quite different, so they come from different universes...?)

[Anatole Dedecker]

This doesn’t answer your question, but I would suggest indexing by bool rather than ˋfin 2`, it makes things less annoying to work with imo

[Jireh Loreaux]

docs#normed_add_comm_group.induced

[Jireh Loreaux]

This takes an additive group monomorphism and pulls back the norm structure (including topological, metric and bornological structures) along the map. Then all you need is this map, but add_equivs should be easy to come by here.

[Alex Kontorovich]

Ok thanks, I'll try it!...

[Jireh Loreaux]

Looks like we don't have a pullback specifically for docs#inner_product_space. @Anatole Dedecker or am I missing it? I figure you are very familiar with this part of the library by now :smile:

[Anatole Dedecker]

I've never seen it and I can't find it either, so we probably don't have it :/

[Anatole Dedecker]

And also if we had it docs#submodule.inner_product_space would probably be defined in terms of it

[Anatole Dedecker]

@Alex Kontorovich just to warn you this is probably going to be a bit painful. If you want to try doing it then go for it, getting experience on how to manage this boilerplate side of the library is certainly valuable. But if you really need it and don't want to spend too much time on this I could have a go at it

[Anatole Dedecker]

(If anyone else wants to tackle it I'd be happy not to have to do it of course, but someone should do it at some point)

[Alex Kontorovich]

Thanks; I seem to have found a work-around for what I need that bypasses this construction... I certainly am not competent in how to manage the boilerplate!...

[Eric Wieser]

A question for down the road: do we want separate pi_Lp r β and prod_Lp r α β, or should we copy docs#lex and have Lp r (Π i, β i) and Lp r (α × β)?

[Eric Wieser]

(I think this is only a question of spelling, it doesn't actually generalize any interesting theorems)

[Eric Wieser]

It does mean that the "copy the algebraic structure" boilerplate is needed once not twice

[Jireh Loreaux]

That's a nice idea, I didn't realize that's how lex works. It took me a few minutes to read and process it.

[Yaël Dillies]

Having authored lex, I unsurprisingly like this approach :grinning:

[Eric Wieser]

Let's not attempt this until the existing ennreal refactor has gone through

[Yaël Dillies]

Did someone implement prod_Lp? If not I'll do it tomorrow.

[Jireh Loreaux]

no, I haven't bothered. I do have a PR implementing equivalence between lp and other spaces sitting on the queue, in case anyone want to review it: #15872

[Moritz Doll]

Yaël Dillies said:

Did someone implement prod_Lp? If not I'll do it tomorrow.

did you do that?

[Tomas Skrivan]

Bump again, is there a progress on prod_Lp? Out of curiosity, why is inf norm on pi and products instead of l2 norm? I'm formalizing some physics and I find this a bit annoying.

[Moritz Doll]

I don't think anyone has done this yet, but pinging @Yaël Dillies anyways. I actually do need this soonish as well. I have zero Lean-time at the moment, but I want to prove that the adjoint is closed and the nice proof uses the Hilbert space structure of the prod_Lp for p = 2.

[Tomas Skrivan]

Should prod_Lp be a def or structure?

I was thinking about the lack of inner product on normal product a bit more. My goal is to compute gradients and I expect to do it on code I have not written, so it will use the normal product and not the specialized product. For example, how should I compute gradient or/and adjoint of uncurry Add.addas it has the wrong product there. Should there be uncurryLp, ProdLp.fst, ProdLp.snd ...?

[Eric Wieser]

It should be a def to match docs#PiLp

[Anatole Dedecker]

Tomas Skrivan said:

I was thinking about the lack of inner product on normal product a bit more. My goal is to compute gradients and I expect to do it on code I have not written, so it will use the normal product and not the specialized product. For example, how should I compute gradient or/and adjoint of uncurry Add.addas it has the wrong product there. Should there be uncurryLp, ProdLp.fst, ProdLp.snd ...?

You can use the fact that composing with docs#ContinuousLinearEquiv preserves differentiability and the fact (not here yet of course) that the "identity" between ProdLp and Prod is a continuous linear equiv. But I see that this could be a bit annoying. Another solution would be to define derivatives independently of the norm, as has been discussed a few times already.

[Tomas Skrivan]

The trouble is not with derivative but with gradient. Gradient is adjoint of the differential and it depends on the inner product structure.

[Eric Wieser]

I feel like any kind of "this is the wrong product" problem can be solved by composing with the Prod version of docs#PiLp.continuousLinearEquiv

[Anatole Dedecker]

The point is that then all results about differentials on products would transfer seemlessly to ProdLp (maybe with a bit of defeq abuse) since the topology is the same.

[Anatole Dedecker]

Eric Wieser said:

I feel like any kind of "this is the wrong product" problem can be solved by composing with the Prod version of docs#PiLp.continuousLinearEquiv

Ah right that's the identity map I was talking about above

[Eric Wieser]

Or at least, it is now that I fixed the link

[Anatole Dedecker]

I remember someone at ICERM last year having to take that approach, and I remember it was a bit annoying.

[Eric Wieser]

For prod or pi?

[Tomas Skrivan]

Ok makes sense but I want a simple push button differentiation and I worry that I would have to fiddle with this identity quite a bit. I will see how bad it gets.

[Anatole Dedecker]

Eric Wieser said:

For prod or pi?

pi. @Heather Macbeth might remember more about it.

[Eric Wieser]

I don't remember exactly when ICERM was, but I did a handful of refactors through mathlib that added the identity where it was missing: this should have made thing better. The problem arises when half your lemmas are stated with defeq abuse, and half with the synonym identity

[Yaël Dillies]

Exactly. Heather was strongly against introducing this identity map because she thought it would induce too much API. In fact we already had the identity map, but the lemmas were not stated with it.

[Anatole Dedecker]

For reference the PR of mine that I had in mind was !3#15363, but indeed I think Eric only added docs#PiLp.continuousLinearEquiv in a subsequent PR.

[Eric Wieser]

I think we might actually have two copies of PiLp.continuousLinearEquiv; I think I remember finding it elsewhere with another name, but it was already ported so I didn't bother cleaning it up...

[Moritz Doll]

I finally took some time and did the huge copy&paste thing so that we have inner products for products: mathlib4#6136