Riesz theorem

Stream: new members

[jsodd]

Is there the Riesz representation theorem in mathlib? Maybe just the simple case, like saying that any linear functional l : (n → ℝ) →L[ℝ] ℝ may be interpreted as a vector n → ℝ. In this case it's easy to do manually, but in other similar situations some theorem would be nice.

[Matthew Ballard]

docs#InnerProductSpace.toDual

[jsodd]

Thanks. For some reason it fails to synthesize InnerProductSpace ℝ (n → ℝ)

[Etienne Marion]

I think this is because (n \to \R) is endowed with infinite norm rather than the euclidean one. You should use docs#PiLp 2 instead I think

[jsodd]

I see... Is there a standard way to switch? That is, if I didn't need the $L^2$ structure up to some point and I don't want to rewrite everything before that, is there a way to use it ad hoc?

[Etienne Marion]

I’ve never used it so I don’t know if it is convenient, but the switch is docs#WithLp.equiv

[Luigi Massacci]

Also we have docs#EuclideanSpace, which is just a wrapper over PiLp, but it looks nicer

[jsodd]

This is great! I still have troubles making n → ℝ out of l : (n → ℝ) →L[ℝ] ℝ, but I guess I'll figure it out. Thank you very much

[jsodd]

In this case I could just take a basis let e := fun (i j : n) \map if i = j then (1 : \R) else (0 : \R) and define let l' := fun (i : n) \map l (e i). I guess it's just easier than going through the all this machinery

[Etienne Marion]

This is docs#Basis.toDualEquiv

[jsodd]

I've tried this:

#check InnerProductSpace.toDualMap ℝ (WithLp 2 (n → ℝ) → ℝ)

but now Lean cannot synthesize NormedAddCommGroup (WithLp 2 (n → ℝ) → ℝ).

[Luigi Massacci]

It would be better probably if you try to give more context for what you want to do

[jsodd]

Well, in the simplest case I'd like to be able to find a unique vector x : n → ℝ representing l : (n → ℝ) →L[ℝ] ℝ relative to the standard scalar product

[jsodd]

And I'd also like to understand how to do this in the general Hilbert space context. But first just the finite dimensional case, as simple as possible

[jsodd]

I'm not yet sure, but this seems to be close to what I'm looking for:

variable {x : (n → ℝ) →L[ℝ] ℝ}
#check (InnerProductSpace.toDual ℝ (WithLp 2 (n → ℝ))).invFun x

[jsodd]

Maybe this belongs somewhere near InnerProductSpace.toDual? Taking linear functional representatives is a very common thing...

[Etienne Marion]

Isn't docs#InnerProductSpace.toDual_symm_apply what you're looking for?

[Etienne Marion]

jsodd said:

#check (InnerProductSpace.toDual ℝ (WithLp 2 (n → ℝ))).invFun x

You should use .symm instead of .invFun to keep a linear equiv

[jsodd]

I want the representative itself, not some lemma about it

[Etienne Marion]

Yes I understand but you already have it, it is

(InnerProductSpace.toDual ℝ (WithLp 2 (n → ℝ))).symm x

[Etienne Marion]

Isn't it?

[jsodd]

Yes. I'm just saying that maybe this operation deserves its own def.

[jsodd]

Just because it's so common to prove something by first proving linearity and then taking representatives

[jsodd]

Etienne Marion said:

You should use .symm instead of .invFun to keep a linear equiv

But the fact that it's linear equivalence is gone as soon as I apply it to x, no?

[Etienne Marion]

Well here it does not matter I think, but generally when you need the inverse of an equiv, you use symm to also have an equiv

[jsodd]

Okay, thanks for the advice!

[jsodd]

One more question on the same subject. Let's say I have defined a function m : (n → ℝ) → ℝ. What do I have to do, after proving h : IsLinearMap m, to reinterpret m as m : (n → ℝ) →L[ℝ] ℝ? What's the proper way to use h?

[Ruben Van de Velde]

@loogle IsLinearMap, LinearMap

[loogle]

:search: IsLinearMap.mk', LinearMap.isLinear, and 2 more

[Ruben Van de Velde]

Presumably h.mk' m will work

[jsodd]

Just h.mk' did the trick, thanks! So it's always through .mk constructors? I mean in similar circumstances

[Ruben Van de Velde]

In similar circumstances, I would also look at what loogle finds :)

[jsodd]

The problem with loogle and the official documentation (which for me is easier to use) is to know how things are called.

[jsodd]

For example, I know what a Riesz representation theorem is, but there seems to be no way to find it in lean by this name

[jsodd]

It would be so nice to have a more user-friendly search

[jsodd]

And something like fzf on linux would also be great. Just to be less punished by the search for not knowing the precise name. Maybe I'll try writing something like this for myself...

[Kevin Buzzard]

If you know the name of the theorem, use moogle.ai

[jsodd]

I just tried to find Riesz representation theorem, but it couldn't.

[Matthew Ballard]

jsodd said:

For example, I know what a Riesz representation theorem is, but there seems to be no way to find it in lean by this name

You can search the repository on Github for "Riesz representation". The name is in the comments (as it should be).

[jsodd]

image.png
I found it in the end by clicking on "Google site search" here

[Matthew Ballard]

It also appears in the library overiew on the community webpage https://leanprover-community.github.io/mathlib-overview.html

[jsodd]

I just hope the search will get easier in the future :smile:

[jsodd]

I know it's far from the current project goals, but it's just so easy to imagine how a more user-friendly search may function.

[Matthew Ballard]

I agree that search can be difficult

[jsodd]

This google search feature seems to be quite good, just found "second dual" theorems with it. In lean it's called "double dual" with no second duals mentioned, but Google knows that double and second are the same thing.