Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-29 01:17 44105f84

View on Github →

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.

Estimated changes

Modified docs/references.bib

Modified docs/undergrad.yaml

Modified src/analysis/inner_product_space/dual.lean

added def inner_product_space.continuous_linear_map_of_bilin

added theorem inner_product_space.continuous_linear_map_of_bilin_apply

added theorem inner_product_space.unique_continuous_linear_map_of_bilin

Created src/analysis/inner_product_space/lax_milgram.lean

added theorem is_coercive.antilipschitz

added theorem is_coercive.bounded_below

added theorem is_coercive.closed_range

added def is_coercive.continuous_linear_equiv_of_bilin

added theorem is_coercive.continuous_linear_equiv_of_bilin_apply

added theorem is_coercive.ker_eq_bot

added theorem is_coercive.range_eq_top

added theorem is_coercive.unique_continuous_linear_equiv_of_bilin

Modified src/analysis/normed_space/operator_norm.lean

added def is_coercive