The Lax-Milgram Theorem #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We consider an Hilbert space V over ℝ equipped with a bounded bilinear form B : V →L[ℝ] V →L[ℝ] ℝ.

Recall that a bilinear form B : V →L[ℝ] V →L[ℝ] ℝ is coercive iff ∃ C, (0 < C) ∧ ∀ u, C * ‖u‖ * ‖u‖ ≤ B u u. Under the hypothesis that B is coercive we prove the Lax-Milgram theorem: that is, the map inner_product_space.continuous_linear_map_of_bilin from analysis.inner_product_space.dual can be upgraded to a continuous equivalence is_coercive.continuous_linear_equiv_of_bilin : V ≃L[ℝ] V.

References #

We follow the notes of Peter Howard's Spring 2020 M612: Partial Differential Equations lecture, see[How]

Tags #

dual, Lax-Milgram

source

theorem is_coercive.bounded_below {V : Type u} [normed_add_comm_group V] [inner_product_space ℝ V] [complete_space V] {B : V →L[ℝ ] V →L[ℝ ] ℝ} (coercive : is_coercive B) :

∃ (C : ℝ), 0 < C ∧ ∀ (v : V), C * ‖v‖ ≤ ‖⇑(inner_product_space.continuous_linear_map_of_bilin B) v‖

source

theorem is_coercive.antilipschitz {V : Type u} [normed_add_comm_group V] [inner_product_space ℝ V] [complete_space V] {B : V →L[ℝ ] V →L[ℝ ] ℝ} (coercive : is_coercive B) :

∃ (C : nnreal), 0 < C ∧ antilipschitz_with C ⇑(inner_product_space.continuous_linear_map_of_bilin B)

source

theorem is_coercive.ker_eq_bot {V : Type u} [normed_add_comm_group V] [inner_product_space ℝ V] [complete_space V] {B : V →L[ℝ ] V →L[ℝ ] ℝ} (coercive : is_coercive B) :

linear_map.ker (inner_product_space.continuous_linear_map_of_bilin B) = ⊥

source

theorem is_coercive.closed_range {V : Type u} [normed_add_comm_group V] [inner_product_space ℝ V] [complete_space V] {B : V →L[ℝ ] V →L[ℝ ] ℝ} (coercive : is_coercive B) :

is_closed ↑(linear_map.range (inner_product_space.continuous_linear_map_of_bilin B))

source

theorem is_coercive.range_eq_top {V : Type u} [normed_add_comm_group V] [inner_product_space ℝ V] [complete_space V] {B : V →L[ℝ ] V →L[ℝ ] ℝ} (coercive : is_coercive B) :

linear_map.range (inner_product_space.continuous_linear_map_of_bilin B) = ⊤

source

noncomputable def is_coercive.continuous_linear_equiv_of_bilin {V : Type u} [normed_add_comm_group V] [inner_product_space ℝ V] [complete_space V] {B : V →L[ℝ ] V →L[ℝ ] ℝ} (coercive : is_coercive B) :

V ≃L[ℝ ] V

The Lax-Milgram equivalence of a coercive bounded bilinear operator: for all v : V, continuous_linear_equiv_of_bilin B v is the unique element V such that ⟪continuous_linear_equiv_of_bilin B v, w⟫ = B v w. The Lax-Milgram theorem states that this is a continuous equivalence.

Equations

coercive.continuous_linear_equiv_of_bilin = continuous_linear_equiv.of_bijective (inner_product_space.continuous_linear_map_of_bilin B) _ _

source

@[simp]

theorem is_coercive.continuous_linear_equiv_of_bilin_apply {V : Type u} [normed_add_comm_group V] [inner_product_space ℝ V] [complete_space V] {B : V →L[ℝ ] V →L[ℝ ] ℝ} (coercive : is_coercive B) (v w : V) :

has_inner.inner (⇑(coercive.continuous_linear_equiv_of_bilin) v) w = ⇑(⇑B v) w

source

theorem is_coercive.unique_continuous_linear_equiv_of_bilin {V : Type u} [normed_add_comm_group V] [inner_product_space ℝ V] [complete_space V] {B : V →L[ℝ ] V →L[ℝ ] ℝ} (coercive : is_coercive B) {v f : V} (is_lax_milgram : ∀ (w : V), has_inner.inner f w = ⇑(⇑B v) w) :

f = ⇑(coercive.continuous_linear_equiv_of_bilin) v