Name for certain map in Hilbert spaces

Stream: maths

[Daniel Roca González]

Hello,

Let $V$ be a real Hilbert space and $B$ a bilinear map on it. Then we can define a continuous map $V \to V$ as follows:
for $v \in V$, map it to the unique vector $f \in V$ such that $\forall w \in V, B(v,w) = \langle f, w\rangle$, which exists because of the Riesz representation theorem. How do we want to call this map? So far I've called it "Lax-Milgram map" because that's where I'm using it (the Lax-Milgram theorem can be stated as saying that this can be made a continuous equivalence under certain conditions), but @Heather Macbeth suggested we put it directly in analysis.inner_product_space.dual and give it a more descriptive name. She gave sharp B, end_of_bilin B and clm_of_bilin B as ideas. What do you think?

[Heather Macbeth]

I hope we can get some ideas here since I am not thrilled about the ones I suggested :). @Frédéric Dupuis @Patrick Massot what do you think?

[Heather Macbeth]

sharp is from the musical isomorphism

[Daniel Roca González]

In differential geometry this operation would be raising an index, so what about "raise"?

[Daniel Roca González]

Alternatively, we are basically converting a bilinear form to an endomorphism, so it could be to_map or to_endo

[Heather Macbeth]

For these latter ideas, this is indeed where I was going with the end_of_bilin and clm_of_bilin (clm for "continuous linear map"), but I think the of_bilin is necessary because it won't literally be in the bilin_form namespace.

[Daniel Roca González]

Yes, that sounds reasonable

[Heather Macbeth]

I quite like raise, though. And remarkably the word is not yet used in mathlib for anything else!

[Heather Macbeth]

By the way, another application of this construction will be when we prove the version of the spectral theorem which says that two symmetric bilinear forms are simultaneously diagonalizable. It would be deduced from the current version for endomorphisms, by converting the second form B to an endomorphism using raise with the first form as the inner product.

[Heather Macbeth]

Ah, perhaps @Moritz Doll would have an opinion here, too.

[Frédéric Dupuis]

I would vote for clm_of_bilin personally, it's completely descriptive and easy to guess if you're looking for it. (Never in a million years would I guess raise :-) )

[Moritz Doll]

maybe cont_linear_map_of_bilin or is that too long? I think clm is not really understandable

[Heather Macbeth]

We could call it continuous_linear_map_of_bilin and have local notation raise for continuous_linear_map_of_bilin, so that it isn't too much a pain to write code about.

[Heather Macbeth]

Or actually (keeping the name as continuous_linear_map_of_bilin), even notation ♯ (for sharp): I think having a series of lemmas about B♯ would look quite pretty and efficient, and it has more outside-mathlib precedent than some of our crazy notation.

[Daniel Roca González]

I kind of agree with the others that raise would not be immediately understandable: having the name continuous_linear_map_of_bilin and having # as local notation could be the best of both worlds.

[Daniel Roca González]

We also should define the inverse map, which works in arbitrary inner product spaces: it could be bilin_of_continuous_linear_map and have the notation ♭

[Patrick Massot]

I like the idea of having a long name and a notation. We already do this, especially in projects depending on mathlib. One catch is that the doc website will show the long version.

[Daniel Roca González]

I think that the correct way to think about the map is that there is a (continuous) map (V →L[ℝ] V) →L[ℝ] (V →L[ℝ] V →L[ℝ] V), which is an equivalence if V is a Hilbert space (and the analogous statement for the complex numbers using is_R_or_C, of course). Then the Lax-Milgram theorem can be stated as saying that bijective continuous linear maps are mapped bijectively to coercive bilinear forms. This does complicate things though...

[Patrick Massot]

We could also decide that we really need a shorter long version of continuous_linear_map. clm is indeed already used in a couple of places, but very few.

[Daniel Roca González]

@Patrick Massot I think showing the explicit version in the docs instead of the obscure notation is a feature, not a bug.

[Patrick Massot]

The ideal situation would be to show the notation with something like a tooltip telling what it means. But clearly this is low priority until Lean 4.

[Heather Macbeth]

Daniel Roca González said:

having # as local notation

Note that I am proposing notation ♯, not # :)

[Daniel Roca González]

how does it work when someone else wants to use ♯ for something else? can they simply define the notation in their own namespace and that's it, or would it be necessary to define a class like has_sharp in the vein of has_add, has_mem...

[Yaël Dillies]

You can wrap notation in locales using localized "the_code_that_you_want_to_be_localized" in name_of_the_locale

[Yaël Dillies]

Look for localized and you'll find a ton of examples in mathlib.

[Heather Macbeth]

In this case, I think it would be fine not to implement either of these methods (localized notation or a has_sharp class), they can wait until someone else actually has a use case for the same notation.

[Daniel Roca González]

So if nobody complains I would go for continuous_linear_map_of_bilin with the musical notation.

[Daniel Roca González]

Is there an explanation of what locales are and how they work anywhere? I'm looking at examples but I don't really understand them vs. namespaces. I didn't find anything in TOPL.

[Reid Barton]

https://leanprover-community.github.io/mathlib_docs/commands.html#localized%20notation

[Daniel Roca González]

Okay so now my problem is as follows: I defined continuous_linear_map_of_bilin in the general is_R_or_C case, with the notation, but if I try B♯ it doesn't work because Lean can't infer the field, so I have to do (B♯ : V →L[ℝ] V) which is worse. Is there anything I could do to fix this?

[Yaël Dillies]

Make the field part of the notation?

[Frédéric Dupuis]

This likely means that we have to give up on localized notation, and use something like

local postfix `♯` := continuous_linear_map_of_bilin 𝕜

after having defined 𝕜.

[Heather Macbeth]

In fact, we have the same problem for the inner product itself. Practically every file on Hilbert spaces starts with

local notation `⟪`x`, `y`⟫` := @inner 𝕜 _ _ x y

because it is more ergonomic to do this (even at the cost of the duplication and the making ⟪v, w⟫ a local notation which doesn't show up in the docs) than to have an ugly notation like 𝕜⟪v, w⟫ or something which explicitly mentions the 𝕜.

[Yaël Dillies]

lol, branch#inner_product_spaces

[Yaël Dillies]

Oh whoops sorry I deleted it. But this branch was using 𝕜⟪v | w⟫ all over the place.

[Sebastien Gouezel]

In the case of continuous_linear_map_of_bilin, doesn't it take as an argument a bilinear map over some field, and then why isn't it possible for Lean to get the field by unification?

[Anne Baanen]

If I remove the type ascriptions at line 74 in src/analysis/inner_product_space/lax_milgram.lean:

lemma bounded_below (coercive : is_coercive B) :
  ∃ C, 0 < C ∧ ∀ v, C * ∥v∥ ≤ ∥(B♯ : V →L[ℝ] V) v∥ :=
begin
  rcases coercive with ⟨C, C_ge_0, coercivity⟩,
  refine ⟨C, C_ge_0, _⟩,
  intro v,
  by_cases h : 0 < ∥v∥,
  { refine (mul_le_mul_right h).mp _,
    exact calc C * ∥v∥ * ∥v∥
               ≤ B v v                         : coercivity v
    ...        = inner (B♯ v) v : by simp
    ...        ≤ ∥B♯ v∥ * ∥v∥     : real_inner_le_norm (B♯ v) v, },
  { have : v = 0 := by simpa using h,
    simp [this], }
end

The error is:

type mismatch at application
  B♯
term
  B
has type
  V →L[ℝ] V →L[ℝ] ℝ : Type u
but is expected to have type
  ?m_3 →L⋆[?m_1] ?m_3 →L[?m_1] ?m_1 : Type (max ? ?)

[Anne Baanen]

I suspect the →L[?m_1] versus →L⋆[?m_1] has something to do with this...

[Anne Baanen]

Right, star_ring_end ℝ is defeq to ring_hom.id ℝ, but star_ring_end ?m_1 is not. So with the type ascription, the elaborator figures out ?m_1 = ℝ, it can unfold star_ring_end ℝ and we're in business. And without the type ascription, it apparently doesn't realize that →L[ℝ] =?= →L⋆[?m_1] implies ?m_1 = ℝ.

[Anne Baanen]

I don't know why the elaborator skips unifying the type-level arguments here:

variables {V : Type u} [inner_product_space ℝ V] [complete_space V]
section
set_option trace.type_context.is_def_eq true
set_option trace.type_context.is_def_eq_detail true
set_option pp.notation false
variables {B₂ : V →L[ℝ] V}
example := (B₂ : V →L⋆[_] V)
end

[type_context.is_def_eq] Type u =?= Type ? ... success  (approximate mode)
[type_context.is_def_eq_detail] [1]: continuous_linear_map (ring_hom.id real) V V =?= continuous_linear_map (star_ring_end ?m_5) V V
[type_context.is_def_eq_detail] [2]: continuous_linear_map =?= continuous_linear_map
[type_context.is_def_eq_detail] [2]: ring_hom.id real =?= star_ring_end ?m_1
[type_context.is_def_eq_detail] [3]: {to_fun := id real, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _} =?= coe star_ring_aut
[type_context.is_def_eq_detail] unfold right: coe
[type_context.is_def_eq_detail] [4]: {to_fun := id real, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _} =?= lift_t star_ring_aut
...

[Anne Baanen]

Aha, type_context_old::is_def_eq_args unifies explicit arguments or implicit arguments of the form t =?= ?m first, before doing implicits. But the problem @continuous_linear_map real real real.semiring real.semiring … =?= @continuous_linear_map ?m_1 … looks like its first argument should be of that form :thinking:

[Anne Baanen]

Ok, I don't feel like stepping through this whole thing in a debugger, and I don't know if it's worth the effort to investigate this if Lean 4 might change this part of the elaborator radically anyway, so I'll leave it here for someone with more elaborator knowledge to investigate.

[Daniel Roca González]

Heather Macbeth said:

In fact, we have the same problem for the inner product itself. Practically every file on Hilbert spaces starts with

local notation `⟪`x`, `y`⟫` := @inner 𝕜 _ _ x y

because it is more ergonomic to do this (even at the cost of the duplication and the making ⟪v, w⟫ a local notation which doesn't show up in the docs) than to have an ugly notation like 𝕜⟪v, w⟫ or something which explicitly mentions the 𝕜.

I has hoping this was not necessary, but if we're using it for the inner product too it makes sense to do it like this here.