Bounded bilinear forms

Stream: new members

[Moritz]

I was playing around with Lax-Milgram and I noticed that the definitions of is_bounded_bilinear_map in analysis/normed_space/bounded_linear_maps and bilinear_form in linear_algebra/bilinear_form are quite different, the former defines a proposition and the later defines the object. Is this intentional or should is_bounded_bilinear_map be a lemma and a new definition bounded_bilinear_map, which is of the same form as the one in linear_algebra/bilinear_form?

[Heather Macbeth]

@Moritz, perhaps you are asking whether the concept is_bounded_bilinear_map should be "bundled". Is that right?

[Heather Macbeth]

That is, you're asking whether it would be better to define something like

structure bounded_bilinear_form extends bilin_form R M :=
(bounded : ∃ (C : ℝ) (H : C > 0), ∀ (x : E) (y : F), ∥f (x, y)∥ ≤ (C * ∥x∥) * ∥y∥)

[Moritz]

I was asking whether one could imitate the definition of bilin_form, but extending it sounds even better

[Heather Macbeth]

I believe this is a case where it was written "unbundled" a long time ago, before bundling everything became the mathlib convention. It seems that @Patrick Massot wrote the first version of this file back in 2018 so he can probably confirm this.

[Heather Macbeth]

Offhand, I would say, yes, it might be good to change to a bundled definition, but it might be a fair bit of work to switch over.

[Heather Macbeth]

For something related which is already bundled, check out docs#continuous_multilinear_map

[Heather Macbeth]

Mathlib often goes through large-scale refactors like this, so if there's a consensus, you'd be welcome to switch it over (but we usually try to save our newcomers from having to do this kind of tedious work :smiley: )

[Kevin Buzzard]

I've actually found that bundling stuff is really educational! Several Imperial students bundled basic algebraic stuff very early on in their career and I'm convinced it taught them a lot. "Look at this file, now try to do the same with this thing"

[Moritz]

I feel it is more tedious to prove Lax-Milgram with the unbundled version :-D

[Heather Macbeth]

(I am delighted to hear someone is attacking Lax-Milgram!)

[Moritz]

Yeah, refactoring the stuff in linear_algebra was really instructive, even though it was not that difficult. I am just afraid that if I start refactoring everything I find, I will never prove anything in Lean

[Eric Rodriguez]

welcome to what we do here ;b

[Patrick Massot]

I don't think I introduced bounded bilinear maps. But I can confirm that nothing was bundled in 2018

[Heather Macbeth]

Ah, in fact it was @Sebastien Gouezel, in #966.

[Heather Macbeth]

Moritz said:

I feel it is more tedious to prove Lax-Milgram with the unbundled version :-D

Moritz said:

I am just afraid that if I start refactoring everything I find, I will never prove anything in Lean

Indeed, there's a bit of "tedious either way" going on here .... but my guess is that it'll be slightly pleasanter (for now) to do it with the existing, unbundled version, feel free to recruit help on Zulip for things that feel harder than they should be.

[Heather Macbeth]

Actually, a third way would be to assume

(B : bilin_form R M) (hB : is_bounded_bilinear_map B)

which is a little redundant (since it's stating the bilinearity twice), but not actually wrong.

[Heather Macbeth]

(I mean, hopefully this would not be what is done in the library in another 3 years from now, but I think it's a perfectly fine hack for now.)

[Moritz]

The issue with not cleaning up now (or soon) is that it will only get more involved the more stuff we build on top of the non-refactored structure.

[Moritz]

I've looked at the linear algebra part of it and I feel like even that is in need of a quite significant cleanup: I think it is possible to unify bilinear_map, bilin_form and sesq_form into a single semibilin_map which has the former three as special cases. The definition could be essentially what is the definition of bilin_form but way more general (yesterday I generalized it to a bilinear map, but not with the ring homomorphism yet). the way that bilin_form is written makes it easy to extend it to a bounded bilinear form, I don't see how to do the same thing with the current definition of the bilinear map.

[Moritz]

Is it ok to do a pull-request with a very much wip version just to get feedback on whether this has any chance of getting accepted into mathlib?

[Johan Commelin]

Certainly! There are RFC and WIP labels that you can use.

[Frédéric Dupuis]

Moritz said:

I've looked at the linear algebra part of it and I feel like even that is in need of a quite significant cleanup: I think it is possible to unify bilinear_map, bilin_form and sesq_form into a single semibilin_map which has the former three as special cases. The definition could be essentially what is the definition of bilin_form but way more general (yesterday I generalized it to a bilinear map, but not with the ring homomorphism yet). the way that bilin_form is written makes it easy to extend it to a bounded bilinear form, I don't see how to do the same thing with the current definition of the bilinear map.

Is there any reason to use these over things like E →ₗ[R] F →ₗ[R] G?

[Notification Bot]

This topic was moved by Anne Baanen to #maths > Bounded bilinear forms

[Frédéric Dupuis]

I was also thinking about this because just yesterday I opened a PR (#10373) to allow semilinear versions of maps of type E →ₗ[R] F →ₗ[R] G, i.e. E →ₛₗ[σ] F →ₛₗ[ρ] G, with [module R₁ E], [module R₂ F] and [module R₃ G], and σ : R₁ →+* R₃, ρ : R₂ →+* R₃. As far as I can tell, this should cover pretty much all cases of interest, so I was wondering if we should just use that systematically and deprecate bilin_form and sesq_form.