Lax-Milgram theorem

[hrmacbeth]

It'd be nice to knock the Lax-Milgram theorem off the undergrad todo list. The only definition needed should be coercive, as a property of 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/Coq blueprint is a possible reference (please give credit in your docs if you use it). These slides give another sketch of the standard proof.

Zulip