Lax-Milgram theorem, todo for someone

Stream: general

[Heather Macbeth]

It'd be nice to knock the Lax-Milgram theorem off the undergrad todo list. I'm recording it here so there's a place to point some future volunteer. The only definition needed should be coercive, as a property of docs#is_bounded_bilinear_map. It relies on the Riesz representation, proved in
https://leanprover-community.github.io/mathlib_docs/analysis/inner_product_space/dual.html
The Coq code is a possible reference (please give credit in your docs if you use it).

[Johan Commelin]

@Heather Macbeth Is this a good candidate for a github issue with the label good-first-project? Currently, all such issues are closed: https://github.com/leanprover-community/mathlib/issues?q=is%3Aissue+label%3Agood-first-project

[Yury G. Kudryashov]

Note that we have a similar fact for the inner product.

[Yury G. Kudryashov]

I might have something very similar for a bilinear form in a local branch. I'll look at this tomorrow.

[Heather Macbeth]

Yury G. Kudryashov said:

Note that we have a similar fact for the inner product.

Yes, this is the Riesz representation theorem!

[Heather Macbeth]

Johan Commelin said:

Heather Macbeth Is this a good candidate for a github issue with the label good-first-project? Currently, all such issues are closed: https://github.com/leanprover-community/mathlib/issues?q=is%3Aissue+label%3Agood-first-project

#10213

[Yury G. Kudryashov]

I meant docs#exists_norm_eq_infi_of_complete_convex

[Yury G. Kudryashov]

I think that we should have this for bilinear forms. And parts of the proof can be simplified using derivatives (unless someone already did that).

[Heather Macbeth]

The Riesz representation theorem depends on this lemma, so it's the same basic ingredients either way. But the way I am thinking of is more abstract-nonsense than what you said. Here are some notes following the way I'm thinking of:
https://www.math.tamu.edu/~phoward/m612/s20/elliptic2.pdf

[Daniel Roca González]

I am thinking about maybe doing this, if nobody else is working on it. Would it be interesting to define a bundled continuous_bilinear_map in the vein of continuous_linear_map and use it, or should I just use what is there?

[Moritz Doll]

I was about to do that, but I somehow got distracted by refactoring bilinear forms. If you want to do it, feel free to do it.

[Moritz Doll]

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Bounded.20bilinear.20forms/near/261995051 for an approach without refactoring

[Daniel Roca González]

I am making progress :) There are still some sorrys, but I think tomorrow I will clean it up a bit, ask for PR permission and upload a WIP version. The outline of the proof is mostly complete (I did it following the slides)

[Daniel Roca González]

https://github.com/leanprover-community/mathlib/pull/11491

[Heather Macbeth]

rss-bot said:

feat(analysis/inner_product_space): proof of the Lax Milgram theorem …
feat(analysis/inner_product_space): proof of the Lax Milgram theorem (#11491)

My work on the Lax Milgram theorem, as suggested by @hrmacbeth. Done following the slides from Peter Howard (Texas A&M University).

Closes #10213.
https://github.com/leanprover-community/mathlib/commit/44105f844202555645b90056efc921128e996ddb

Thanks @Daniel Roca González for this very elegant first contribution!